• 使用课程主页提供的教材英文版本
  • 平时作业独立完成
  • 如果和同学讨论后做出来的需在提交时说明
  • 平时作业周四上课前提交，发送到助教的邮箱，邮件标题请以“学号-姓名”的格式书写
  • Coq源文件不要修改名字，测试环境说明如下：
    • 无论以文件或压缩包提交，测试时只使用其中的.v源文件
    • 同一人提交的所有作业放在同一目录下，使用”coqc -Q . LF <file.v>“选项编译
    • （因而）后一次提交的作业可以使用前面证明过的结论（无论是本来就有的还是自己额外证明的）
  • 第1次作业 2022/02/24 课程介绍 不需要提交
  • 第2次作业 2022/02/28 Basics: Functional Programming in Coq 2022/03/09 截止
    • 完成Bascis.v中standard非optional的11道习题
  • 第3次作业 2022/03/03 Induction: Proof by Induction 等 2022/03/09 截止
    • 完成Induction.v中standard非optional的4道习题
    • 完成Lists.v中standard非optional的11道习题
  • 第4次作业 2022/03/10 Tactics: More Tactics 2022/03/16 截止
    • 完成Poly.v中standard非optional且不属于Additional Exercises的6道习题
    • 完成Tactics.v中standard非optional且不属于Additional Exercises的8道习题
    （可选）如果之前没有接触过函数式语言，可以考虑做一下Poly中Additional Exercises中的习题
  • 第5次作业 2022/03/17 Logic: Logic in Coq 等 2022/03/23 截止
    • 完成Logic.v中standard非optional且不在下面列表中的14道习题
    tr_rev_correct、even_double_conv、eqb_list
  • 第6次作业 2022/03/24 ProofObjects: The Curry-Howard Correspondence 2022/03/30 截止
    • 完成ProofObject中standard非optional的7道习题
  • 第7次作业 2022/03/28 IndProp: Inductively Defined Propositions 等 2022/04/06 截止
    • 完成IndProp中standard非optional截止到case study（不含）之前的5道习题
    • 完成IndPrinciples中standard非optional的3道习题
  • 第8次作业 2022/03/31 Maps: Total and Partial Maps 等 2022/04/13 截止
    • 完成Maps中2道standard非optional的习题
    • 完成Imp中standard非optional并不属于Additional Exercises的6道习题
    从本章起证明长度有显著增加，请尽早动手
  • 2022/04/07 AUTO: More Automation 2022/04/13 截止
    无（可以使用auto策略继续完成上周的作业）
  • 第9次作业 2022/04/11 EQUIV: Program Equivalence 2022/04/20 截止
    • 完成Equiv中standard非optional并不属于Extended/Additional Exercises的9道习题
    推荐完成Nondeterministic Imp部分的两道习题
  • 第10次作业 2022/04/14 Hoare: Haore Logic, Part I 2022/04/27 截止
    • 完成Hoare中standard非optional并不属于Additional Exercises的11道习题
    推荐也完成Havoc部分的习题
  • 第11次作业 2022/04/21 Hoare2: Haore Logic, Part II 2022/05/04 截止
    • 完成Hoare2中standard非optional的5道习题和slow_assignment_dec
  • 第12次作业 2022/04/28 HoareAsLogic: Haore Logic as a Logic 2022/05/11 截止
    • 完成HoareAsLogic中的6道习题
  • 第13次作业 2022/05/09 SmallStep: Small-Step Operational Semantics 2022/05/18 截止
    • 完成SmallStep中standard非optional并不属于Additional Exercises的8道习题
    如有时间，推荐完成par_body_n__Sn
  • 第14次作业 2022/05/12 Types: Type Systems 2022/05/18 截止
    • 完成Types中standard非optional并不属于Additional Exercises的5道习题
  • 第15次作业 2022/05/19 STLC: The Simply Typed Lambda-Calculus 等 2022/05/25 截止
    • 完成STLC中standard非optional的3道习题以及typing_nonexample_3
    • 完成STLCPROP中progress_from_term_ind和unique_types
  • 第16次作业 2022/05/23 MORESTLC: More on the Simply Typed Lambda-Calculus 等 2022/06/01 截止
    • 完成MoreSTLC中standard非optional的5道习题
  • 2022/05/26 REFERENCES: Typing Mutable References 2022/06/01 截止
    无
  • 第17次作业 2022/06/02 Sub: Subtyping 2022/06/08 截止
    • subtype_instances_tf_2, subtype_concepts_tf, small_large_4, sub_inversion_arrow, variations
  • 2022/06/06 Separation Logic: a Quick Look 2022/06/23 截止
    无
  • 2022/06/09 习题课：总复习 2022/06/23 截止
    祝大家考试顺利！