在这里可以下载课程讲义。
-
2021/03/12
胡振江
导言：软件理论基础与实践
[幻灯片]
Basics: Functional Programming in Coq
[幻灯片]
[作业]
-
2021/03/16
胡振江
Induction: Proof by Induction
[幻灯片]
List: Working with Structured Data
[幻灯片]
[作业]
-
2021/03/19
胡振江
Polymorphism and Higher-Order Functions
[幻灯片]
[作业]
-
2021/03/26
胡振江
Tactics: More Basic Tactics
[幻灯片]
[作业]
-
2021/03/30
胡振江
Logic: Logic in Coq
[幻灯片]
-
2021/03/30
胡振江
Logic: Logic in Coq
[幻灯片]
[作业]
-
2021/04/09
熊英飞
ProofObjects: The Curry Howard Correspondence
IndPrinciples: Induction Principles
[幻灯片]
[作业]
-
2021/04/13
熊英飞
IndProp: Inductively Defined Propositions
[幻灯片]
[作业]
-
2021/04/16
熊英飞
Maps: Total and Partial Maps
[幻灯片]
Imp: Simple Imperative Programs
[幻灯片]
[作业]
-
2021/04/23
熊英飞
AUTO: More Automation
[幻灯片]
-
2021/04/27
熊英飞
EQUIV: Program Equivalence
[幻灯片]
[作业]
-
2021/05/07
熊英飞
Hoare: Haore Logic, Part I
[幻灯片]
[作业]
-
2021/05/11
熊英飞
Hoare2: Haore Logic, Part II
[幻灯片]
[作业]
-
2021/05/14
熊英飞
HoareAsLogic : Haore Logic as a Logic
[幻灯片]
[作业]
-
2021/05/21
熊英飞
SmallStep : Small Step Operational Semantics
[幻灯片]
[作业]
-
2021/05/25
熊英飞
Types: Type Systems
[幻灯片]
STLC: The Simply Typed Lambda Calculus
[幻灯片]
[作业]
-
2021/05/28
熊英飞
STLCPROP: Properties of STLC
[幻灯片]
MORESTLC: More on the Simply Typed Lambda Calculus
[幻灯片]
[作业]
-
2021/06/04
熊英飞
TYPECHECKING: A Typechecker for STLC
[幻灯片]
REFERENCES: Typing Mutable References
[幻灯片]
-
