• 使用课程主页提供的英文教材最新版本；
  • 平时作业独立完成，和其他同学讨论的部分需在提交时说明；
  • 当周作业需于下周四上课前提交至教学网（如果 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 道习题。