在这里可以下载课程讲义。
-
-
2022/02/28
Basics: Functional Programming in Coq
[幻灯片]
[作业]
-
2022/03/03
Induction: Proof by Induction
[幻灯片]
Lists: Working with Structured Data
[幻灯片]
Poly: Polymorphism and Higher-Order Functions
[幻灯片]
[作业]
-
-
-
2022/03/24
ProofObjects: The Curry-Howard Correspondence
[幻灯片]
[作业]
-
2022/03/28
IndProp: Inductively Defined Propositions
[幻灯片]
IndPrinciples: Induction Principles
[幻灯片]
[作业]
-
2022/03/31
Maps: Total and Partial Maps
[幻灯片]
Imp: Simple Imperative Programs
[幻灯片]
第二次习题课
[幻灯片]
[作业]
-
-
2022/04/11
EQUIV: Program Equivalence
[幻灯片]
[作业]
-
2022/04/14
Hoare: Haore Logic, Part I
[幻灯片]
[作业]
-
2022/04/21
Hoare2: Haore Logic, Part II
[幻灯片]
[作业]
-
2022/04/28
HoareAsLogic: Haore Logic as a Logic
[幻灯片]
[作业]
-
2022/05/09
SmallStep: Small-Step Operational Semantics
[幻灯片]
[作业]
-
-
2022/05/19
STLC: The Simply Typed Lambda-Calculus
[幻灯片]
STLCPROP: Properties of STLC
[幻灯片]
[作业]
-
2022/05/23
MORESTLC: More on the Simply Typed Lambda-Calculus
[幻灯片]
TYPECHECKING: A Typechecker for STLC
[幻灯片]
[作业]
-
2022/05/26
REFERENCES: Typing Mutable References
[幻灯片]
[作业]
-
-
2022/06/06
Separation Logic: a Quick Look
[幻灯片]
[作业]
-
