作业
- 使用课程主页提供的英文教材最新版本
- 作业独立完成，和其他同学讨论的部分需在提交时说明
- 平时作业发送到助教的邮箱（cyy9447@pku.edu.cn），邮件标题请以“
学号-姓名”的格式书写 - 作业提交要求：只需提交
.v文件，并且请勿修改文件名
-
2023/02/23 课程介绍 不需要提交
- 下载教科书及相关Coq代码 ：https://softwarefoundations.cis.upenn.edu
- 安装Coq系统和至少一个开发环境 ：https://coq.inria.fr/download
-
2023/02/27 Basics: Functional Programming in Coq 2023/03/08 截止
- 完成Bascis.v中standard非optional的11道习题（请使用最新版本英文教材）
-
2023/03/02 Induction: Proof by Induction 等 2023/03/12 截止
- 完成Induction.v中standard非optional的6道习题
- 完成Lists.v中standard非optional的11道习题
-
2023/03/09 Poly: Polymorphism and Higher-Order Functions 2023/03/15 截止
- 完成Poly.v中standard非optional且不属于Additional Exercises的7道习题
（可选，不评分）如果之前没有接触过函数式语言，可以尝试Poly中Additional Exercises中的习题 -
2023/03/13 Tactics: More Tactics 2023/03/22 截止
- 完成Tactics.v中standard非optional且不属于Additional Exercises的8道习题
-
2023/03/16 Logic: Logic in Coq 等 2023/03/26 截止
- 完成Logic.v中standard非optional且不在下面列表中的14道习题
tr_rev_correct、even_double_conv、eqb_list -
2023/03/27 ProofObjects: The Curry-Howard Correspondence 2023/04/05 截止
- 完成ProofObject中standard非optional的9道习题
-
2023/03/30 IndProp: Inductively Defined Propositions 等 2023/04/09 截止
- 完成IndProp中standard非optional截止到case study（不含）之前的5道习题
- 完成IndPrinciples中standard非optional的3道习题
-
2023/04/06 Maps: Total and Partial Maps 等 2023/04/16 截止
- 完成Maps中2道standard非optional的习题
- 完成Imp中standard非optional并不属于Additional Exercises的6道习题
从本章起证明长度有显著增加，请尽早动手 -
2023/04/13 EQUIV: Program Equivalence 等 2023/04/23 截止
- 完成Equiv中standard非optional并不属于Extended/Additional Exercises的9道习题
推荐完成Nondeterministic Imp部分的两道习题 -
2023/04/20 Hoare: Hoare Logic, Part I 2023/04/30 截止
- 完成Hoare中standard非optional并不属于Additional Exercises的11道习题
推荐也完成Havoc部分的习题 -
2023/04/27 Hoare2: Hoare Logic, Part II 2023/05/07 截止
- 完成Hoare2中standard非optional的4道习题
-
2023/05/08 HoareAsLogic: Hoare Logic as a Logic 2023/05/17 截止
- 完成HoareAsLogic中的6道习题
-
2023/05/11 SmallStep: Small-Step Operational Semantics 2023/05/17 截止
- 完成SmallStep中standard非optional并不属于Additional Exercises的8道习题
如有时间，推荐完成par_body_n__Sn -
2023/5/18 Types: Type Systems 等 2023/05/28 截止
- 完成Types中standard非optional并不属于Additional Exercises的5道习题
- 完成STLC中standard非optional的3道习题以及typing_nonexample_3
- 完成STLCPROP中progress_from_term_ind和unique_types
-
2023/05/22 MORESTLC: More on the Simply Typed Lambda-Calculus 2023/05/31 截止
- 完成MoreSTLC中standard非optional的6道习题
-
2023/05/25 TYPECHECKING: A Typechecker for STLC 等 2023/05/31 截止
- 完成TypeChecking中type_check_defn和ext_type_checking_sound的•Sums•Lists•Fix
-
2023/06/05 Sub: Subtyping 2023/06/11 截止
- subtype_instances_tf_2, subtype_concepts_tf, small_large_4, sub_inversion_arrow, variations