• 使用课程主页提供的英文教材最新版本
  • 平时作业独立完成，和其他同学讨论的部分需在提交时说明
  • 作业周四上课前提交(如果slides之中有特殊标注，以slides为准)，发送到助教的邮箱（willhuang@stu.pku.edu.cn），邮件标题请以“学号-姓名”的格式书写
  • 作业提交要求：只需提交.v文件，并且请勿修改文件名
  • 第1次作业 2025/02/20 课程介绍 不需要提交
  • 第2次作业 2025/02/25 Basics: Functional Programming in Coq 2025/03/06 13:00 截止
    • 完成Bascis.v中standard非optional的11道习题,More Exercise下的习题除外
  • 第3次作业 2025/02/27 Induction: Proof by Induction 等 2025/03/10 13:00 截止
    • 完成Induction.v中standard非optional的6道习题
    • 完成Lists.v中standard非optional的11道习题
  • 第4次作业 2025/03/06 Poly: Polymorphism and Higher-Order Functions 2025/03/13 13:00 截止
    • 完成Poly.v中standard非optional且不属于Additional Exercises的7道习题
    （可选，不评分）如果之前没有接触过函数式语言，可以尝试Poly中Additional Exercises中的习题
  • 第5次作业 2025/03/11 Tactics: More Tactics 2025/03/20 13:00 截止
    • 完成Tactics.v中standard非optional且不属于Additional Exercises的8道习题
  • 第6次作业 2025/03/13 Logic: Logic in Coq 2025/03/27 13:00 截止
    • 完成Logic.v中standard非optional且不在下面列表中的17道习题
    tr_rev_correct、even_double_conv、eqb_list
  • 第7次作业 2025/03/20 Logic: Logic in Coq 等 2025/03/27 13:00 截止
    • 完成Logic.v中standard非optional且不在下面列表中的17道习题
    tr_rev_correct、even_double_conv、eqb_list
  • 第8次作业 2025/03/25 ProofObjects: The Curry-Howard Correspondence 等 2025/04/03 13:00 截止
    • 完成ProofObject中standard非optional的10道习题
  • 第9次作业 2025/03/27 IndProp: Inductively Defined Propositions 等 2025/04/03 13:00 截止
    • 完成IndProp中standard非optional截止到case study（不含）之前且不包括如下题目的8道习题：le_facts, plus_le_facts1, plus_le_facts2
    • 完成IndPrinciples中standard非optional的3道习题
  • 第10次作业 2025/04/03 Maps: Total and Partial Maps 等 2025/04/10 13:00 截止
    • 完成Maps中2道standard非optional的习题
    • 完成Imp中standard非optional并不属于Additional Exercises的6道习题
  • 第11次作业 2025/04/10 EQUIV: Program Equivalence 等 2025/04/17 13:00 截止
    • 完成Equiv中standard非optional并不属于Extended/Additional Exercises的9道习题
    推荐完成Nondeterministic Imp部分的两道习题
  • 第12次作业 2025/04/17 Hoare: Hoare Logic, Part I 2025/04/24 13:00 截止
    • 完成Hoare中standard非optional并不属于Additional Exercises的10道习题
    推荐也完成Havoc部分的习题
  • 第13次作业 2025/04/22 Hoare2: Hoare Logic, Part II 2025/05/01 13:00 截止
    • 完成Hoare2中standard非optional的4道习题
  • 第14次作业 2025/04/24 HoareAsLogic: Hoare Logic as a Logic 等 2025/05/01 13:00 截止
    • 完成HoareAsLogic中的6道习题
    祝大家五一快乐！
  • 第15次作业 2025/05/08 SmallStep: Small-Step Operational Semantics 2025/05/15 13:00 截止
    • 完成SmallStep中standard非optional并不属于Additional Exercises的8道习题
    如有时间，推荐完成par_body_n__Sn
  • 第16次作业 2025/5/15 Types: Type Systems 等 2025/05/22 13:00 截止
    • 完成Types中standard非optional并不属于Additional Exercises的5道习题
    • 完成STLC中standard非optional的3道习题以及typing_nonexample_3
    • 完成STLCPROP中progress_from_term_ind和unique_types
  • 第17次作业 2025/05/20 MORESTLC: More on the Simply Typed Lambda-Calculus 2025/05/29 13:00 截止
    • 完成MoreSTLC中standard非optional的6道习题
  • 第18次作业 2025/05/22 TYPECHECKING: A Typechecker for STLC 等 2025/05/29 13:00 截止
    • 完成TypeChecking中type_check_defn和ext_type_checking_sound的•Sums•Lists•Fix
  • 第19次作业 2025/05/29 REFERENCES: Typing Mutable References 等 2023/06/05 13:00 截止
    • subtype_instances_tf_2, subtype_concepts_tf, small_large_4, sub_inversion_arrow, variations
  • 2023/06/05 第三次习题课：总复习 不需要提交
    祝大家期末考试顺利！