• 使用课程主页提供的英文教材最新版本；
  • 平时作业独立完成，和其他同学讨论的部分需在提交时说明；
  • 当周作业需于下周四上课前提交至教学网（如果 slides 之中有特殊标注，以 slides 为准）；
  • 作业提交要求：只需提交当次作业涉及到的 Rocq 源文件（.v），无需压缩，且不要修改文件名。
  • 2026/03/05 课程介绍 不需要提交
    祝大家学习愉快！
  • 2026/03/10 Basics: Functional Programming in Rocq 2026/03/19 13:00 截止
    • 完成 Bascis.v 中 standard 非 optional 的习题，More Exercise 下的 Course Late Policies 除外，共 11 道。
  • 2026/03/12 Induction: Proof by Induction 等 2026/03/19 13:00 截止
    • 完成 Induction.v 中 standard 非 optional 的 6 道习题。
    • 完成 Lists.v 中 standard 非 optional 的 10 道习题。
    本周作业量较大，请尽早动手完成。
  • 2026/03/19 Poly: Polymorphism and Higher-Order Functions 2026/03/26 13:00 截止
    • 完成 Poly.v 中 standard 非 optional 且不属于 Additional Exercises 的 7 道习题。
    （可选）如果之前没有接触过函数式语言，可以考虑做一下 Additional Exercises 中的习题，其中第二部分是关于丘奇数的习题。
  • 2026/03/24 Tactics: More Tactics 2026/04/02 13:00 截止
    • 完成 Tactics.v 中 standard 非 optional 且不属于 Additional Exercises 的 9 道习题。
  • 2026/03/26 Logic: Logic in Rocq 2026/04/09 13:00 截止
    • 完成 Logic.v 中 standard 非 optional 且不在下面列表中的 17 道习题。
    tr_rev_correct, even_double_conv, eqb_list
  • 2026/04/02 Logic: Logic in Rocq 2026/04/09 13:00 截止
    • 完成 Logic.v 中 standard 非 optional 且不在下面列表中的 17 道习题。
    tr_rev_correct, even_double_conv, eqb_list
  • 2026/04/07 ProofObjects: The Curry-Howard Correspondence 2026/04/16 13:00 截止
    • 完成 ProofObject.v 中 standard 非 optional 的 10 道习题。
  • 2026/04/09 IndProp: Inductively Defined Propositions 等 2026/04/16 13:00 截止
    • 完成 IndProp.v 中 standard 非 optional 截止到 Case Study（不含）之前且不包括如下题目的 8 道习题。
    le_facts, plus_le_facts1, plus_le_facts2
  • 2026/04/16 IndPrinciples: Induction Principles 等 2026/04/23 13:00 截止
    • 完成 IndPrinciples.v 中 standard 非 optional 的 3 道习题。
    • 完成 Maps.v 中 standard 非 optional 的 2 道习题。
  • 2026/04/21 Imp: Simple Imperative Programs 等 2026/04/30 13:00 截止
    • 完成 Imp.v 中 standard 非 optional 并不属于 Additional Exercises 的 6 道习题。
    从本章起证明长度有显著增加，请尽早动手。
  • 2026/04/23 EQUIV: Program Equivalence 2026/05/07 13:00 截止
    • 完成 Equiv.v 中 standard 非 optional 并不属于 Extended/Additional Exercises 的 8 道习题。
    （可选）推荐也完成 Nondeterministic Imp 部分的两道习题。
  • 2026/04/30 EQUIV: Program Equivalence 等 2026/05/07 13:00 截止
    • 完成 Equiv.v 中 standard 非 optional 并不属于 Extended/Additional Exercises 的 8 道习题。
    （可选）推荐也完成 Nondeterministic Imp 部分的两道习题。
    祝大家五一快乐！
  • 2026/05/07 Hoare2: Hoare Logic, Part II 2026/05/14 13:00 截止
    • 完成 Hoare.v 中 standard 非 optional 并不属于 Additional Exercises 的 10 道习题。
    （可选）推荐也完成 Havoc 部分的习题。
  • 2026/05/14 Hoare2: Hoare Logic, Part II 等 2026/05/21 13:00 截止
    • 完成 Hoare2.v 中 standard 非 optional 的 3 道习题。
  • 2026/05/19 HoareAsLogic: Hoare Logic as a Logic 2026/05/28 13:00 截止
    • 完成 HoareAsLogic.v 中的 6 道习题。
  • 2026/05/21 SmallStep: Small-Step Operational Semantics 等 2026/05/28 13:00 截止
    • 完成 SmallStep.v 中 standard 非 optional 并不属于 Additional Exercises 的 8 道习题。
    （可选）推荐完成 par_body_n__Sn。
    • 完成 Types.v 中 standard 非 optional 并不属于 Additional Exercises 的 5 道习题。
  • 2026/05/28 STLC: The Simply Typed Lambda-Calculus 等 2026/06/04 13:00 截止
    • 完成 Stlc.v 中 standard 非 optional 的 3 道习题以及 typing_nonexample_3。
    • 完成 StlcProp.v 的 progress_from_term_ind 和 unique_types。
  • 2026/06/02 MORESTLC: More on the Simply Typed Lambda-Calculus 等 2026/06/11 13:00 截止
    • 完成 MoreStlc.v 中 standard 非 optional 的 6 道习题。
    • 完成 TypeChecking.v 中 (type_check_defn 和 ext_type_checking_sound) 的 Sums, Lists, Fix。
  • 2026/06/04 REFERENCES: Typing Mutable References 等 不需要提交
    无
  • 2026/06/11 Sub: Subtyping 等 2026/06/21 13:00 截止
    • 完成 Sub.v 中的 subtype_instances_tf_2, subtype_concepts_tf, small_large_4, sub_inversion_arrow, variations。
    祝大家期末考试顺利！