在这里可以下载课程讲义。
-
-
2023/02/27
Basics: Functional Programming in Coq
[幻灯片]
[作业]
-
2023/03/02
Induction: Proof by Induction
[幻灯片]
Lists: Working with Structured Data
[幻灯片]
[作业]
-
2023/03/09
Poly: Polymorphism and Higher-Order Functions
[幻灯片]
[作业]
-
-
-
2023/03/27
ProofObjects: The Curry-Howard Correspondence
[幻灯片]
[作业]
-
2023/03/30
IndProp: Inductively Defined Propositions
[幻灯片]
IndPrinciples: Induction Principles
[幻灯片]
[作业]
-
2023/04/06
Maps: Total and Partial Maps
[幻灯片]
Imp: Simple Imperative Programs
[幻灯片]
[作业]
-
2023/04/10
AUTO: More Automation
[幻灯片]
-
-
2023/04/20
Hoare: Hoare Logic, Part I
[幻灯片]
[作业]
-
2023/04/27
Hoare2: Hoare Logic, Part II
[幻灯片]
[作业]
-
2023/05/08
HoareAsLogic: Hoare Logic as a Logic
[幻灯片]
[作业]
-
2023/05/11
SmallStep: Small-Step Operational Semantics
[幻灯片]
[作业]
-
2023/5/18
Types: Type Systems
[幻灯片]
STLC: The Simply Typed Lambda-Calculus
[幻灯片]
STLCPROP: Properties of STLC
[幻灯片]
[作业]
-
2023/05/22
MORESTLC: More on the Simply Typed Lambda-Calculus
[幻灯片]
[作业]
-
2023/05/25
TYPECHECKING: A Typechecker for STLC
[幻灯片]
第三次习题课
[幻灯片]
[作业]
-
2023/06/01
REFERENCES: Typing Mutable References
[幻灯片]
-
-
2023/06/08
Separation Logic: a Quick Look
[幻灯片]
