课程讲义

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

• 2024/02/22

  课程介绍 [幻灯片]

  [作业]
  
• 2024/02/27

  Basics: Functional Programming in Coq [幻灯片]

  [作业]
  
• 2024/02/29

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

  [作业]
  
• 2024/03/07

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

  [作业]
  
• 2024/03/12

  Tactics: More Tactics [幻灯片]

  [作业]
  
• 2024/03/14

  Logic: Logic in Coq [幻灯片]

  [作业]
  
• 2024/03/21

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

  [作业]
  
• 2024/03/26

  IndProp: Inductively Defined Propositions [幻灯片]
  IndPrinciples: Induction Principles [幻灯片]

  [作业]
  
• 2024/03/26

  IndPrinciples: Induction Principles [幻灯片]
  Maps: Total and Partial Maps [幻灯片]
  第一次习题课 [幻灯片]

  [作业]
  
• 2024/04/09

  Imp: Simple Imperative Programs [幻灯片]

  [作业]
  
• 2024/04/10

  AUTO: More Automation [幻灯片]

  
  
• 2024/04/18

  EQUIV: Program Equivalence [幻灯片]

  [作业]
  
• 2023/04/23

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

  [作业]
  
• 2023/04/25

  Hoare2: Hoare Logic, Part II [幻灯片]

  [作业]
  
• 2023/05/07

  HoareAsLogic: Hoare Logic as a Logic [幻灯片]
  第二次习题课 [幻灯片]

  [作业]
  
• 2023/05/09

  SmallStep: Small-Step Operational Semantics [幻灯片]

  [作业]
  
• 2023/5/16

  Types: Type Systems [幻灯片]
  STLC: The Simply Typed Lambda-Calculus [幻灯片]
  STLCPROP: Properties of STLC [幻灯片]

  [作业]
  
• 2023/05/21

  MORESTLC: More on the Simply Typed Lambda-Calculus [幻灯片]

  [作业]
  
• 2023/05/23

  TYPECHECKING: A Typechecker for STLC [幻灯片]
  第三次习题课 [幻灯片]

  [作业]
  
• 2023/05/30

  REFERENCES: Typing Mutable References [幻灯片]

  
  
• 2023/06/04

  Sub: Subtyping [幻灯片]
  Separation Logic: a Quick Look [幻灯片]

  [作业]