课程讲义

在这里可以下载课程讲义。

• 2025/02/20

  课程介绍 [幻灯片]

  [作业]
  
• 2025/02/25

  Basics: Functional Programming in Coq [幻灯片]

  [作业]
  
• 2025/02/27

  Induction: Proof by Induction [幻灯片]
  Lists: Working with Structured Data [幻灯片]

  [作业]
  
• 2025/03/06

  Poly: Polymorphism and Higher-Order Functions [幻灯片]

  [作业]
  
• 2025/03/11

  Tactics: More Tactics [幻灯片]

  [作业]
  
• 2025/03/13

  Logic: Logic in Coq [幻灯片]

  [作业]
  
• 2025/03/20

  Logic: Logic in Coq [幻灯片]
  ProofObjects: The Curry-Howard Correspondence [幻灯片]

  [作业]
  
• 2025/03/25

  ProofObjects: The Curry-Howard Correspondence [幻灯片]
  IndProp: Inductively Defined Propositions [幻灯片]

  [作业]
  
• 2025/03/27

  IndProp: Inductively Defined Propositions [幻灯片]
  IndPrinciples: Induction Principles [幻灯片]
  第一次习题课 [幻灯片]

  [作业]
  
• 2025/04/03

  Maps: Total and Partial Maps [幻灯片]
  Imp: Simple Imperative Programs [幻灯片]

  [作业]
  
• 2025/04/08

  AUTO: More Automation [幻灯片]

  
  
• 2025/04/10

  EQUIV: Program Equivalence [幻灯片]
  Hoare: Hoare Logic, Part I [幻灯片]

  [作业]
  
• 2025/04/17

  Hoare: Hoare Logic, Part I [幻灯片]

  [作业]