课程讲义

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

• 2026/03/05

  课程介绍 [幻灯片]

  [作业]
  
• 2026/03/10

  Basics: Functional Programming in Rocq [幻灯片]

  [作业]
  
• 2026/03/12

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

  [作业]
  
• 2026/03/19

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

  [作业]
  
• 2026/03/24

  Tactics: More Tactics [幻灯片]

  [作业]
  
• 2026/03/26

  Logic: Logic in Rocq [幻灯片]

  [作业]
  
• 2026/04/02

  Logic: Logic in Rocq [幻灯片]

  [作业]
  
• 2026/04/07

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

  [作业]
  
• 2026/04/09

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

  [作业]