• 平时作业独立完成
  • 如果和同学讨论后做出来的需在提交时说明
  • 平时作业周⼆上课前提交，发送到助教的邮箱，邮件标题请以“2021/MM/DD-SF-学号-姓名”的格式书写
  • Coq源文件不要修改名字，如果打包提交，压缩包请命名为“2021MMDD-SF-学号-姓名”，测试环境说明如下：
    • 同一人提交的所有作业放在同一目录下，使用”coqc -Q . LF <file.v>“选项编译
    • （因而）后一次提交的作业可以使用前面证明过的结论（无论是本来就有的还是自己额外证明的）
  • 第1次作业 2021/03/12 胡振江： 导言：软件理论基础与实践 等 不需要提交
  • 第2次作业 2021/03/16 胡振江： Induction: Proof by Induction 等 2021/03/30 截止
    • 完成Basics.v中的⾄少10个练习题。
    • 完成Induction.v中的⾄少10个练习题。
  • 第3次作业 2021/03/19 胡振江： Polymorphism and Higher-Order Functions 2021/03/30 截止
    • 完成Lists.v中的⾄少10个练习题。
    • 完成Poly.v中的⾄少10个练习题。
  • 第4次作业 2021/03/26 胡振江： Tactics: More Basic Tactics 2021/04/13 截止
    • 完成Tactics.v中的⾄少10个练习题。
  • 第5次作业 2021/03/30 胡振江： Logic: Logic in Coq 2021/04/13 截止
    • 完成Logic.v中的⾄少10个练习题。
  • 第6次作业 2021/04/09 熊英飞： ProofObjects: The Curry Howard Correspondence
    IndPrinciples: Induction Principles     2021/04/13 截止
    • 完成ProofObject、IndPrinciples中standard非optional的习题。
    请使用最新英文版教材。
    注意IndPrinciples中Induction Principles for Propositions的部分将在下次课介绍，该部分无习题。
  • 第7次作业 2021/04/13 熊英飞： IndProp: Inductively Defined Propositions 2021/04/27 截止
    • 完成IndProp中standard非optional截止到case study（不含）之前的习题。
    请使用最新英文版教材。
  • 第8次作业 2021/04/16 熊英飞： Maps: Total and Partial Maps 等 2021/04/27 截止
    • 完成Maps中2道standard非optional的习题和t_update_eq。
    • 完成Imp中standard非optional并不属于Additional Exercises的习题。
    请使用最新英文版教材。
  • 第9次作业 2021/04/27 熊英飞： EQUIV: Program Equivalence 2021/05/11 截止
    • 完成Equiv中standard非optional并不属于Additional Exercises的习题。
    请使用最新英文版教材。
  • 第10次作业 2021/05/07 熊英飞： Hoare: Haore Logic, Part I 2021/05/25 截止
    • 完成Hoare中standard非optional并不属于Additional Exercises的11道习题。
    请使用最新英文版教材。
    推荐也完成Havoc部分的习题。
  • 第11次作业 2021/05/11 熊英飞： Hoare2: Haore Logic, Part II 2021/05/25 截止
    • 完成Hoare2中standard非optional习题。
    请使用最新英文版教材。
  • 第12次作业 2021/05/14 熊英飞： HoareAsLogic : Haore Logic as a Logic 2021/05/25 截止
    • 完成HoareLogic中的习题。
    请使用最新英文版教材。
  • 第13次作业 2021/05/21 熊英飞： SmallStep : Small Step Operational Semantics 2021/05/28 截止
    • 完成SmallStep中standard非optional并不属于Additional Exercises的习题。
    请使用最新英文版教材。
  • 第14次作业 2021/05/25 熊英飞： Types: Type Systems 等 2021/05/28 截止
    • 完成STLC中standard非optional的3道习题以及typing_nonexample_3。
    • 完成Types中standard非optional并不属于Additional Exercises的习题。
    请使用最新英文版教材。
  • 第15次作业 2021/05/28 熊英飞： STLCPROP: Properties of STLC 等 2021/06/04 截止
    • 完成progress_from_term_ind和unique_types。
    • 完成MoreSTLC中standard非optional的习题。
    请使用最新英文版教材。
  • 第16次作业 2021/06/08 熊英飞： Sub: Subtyping 2021/06/18 截止
    • subtype_instances_tf_2
    • subtype_concepts_tf
    • small_large_4
    • sub_inversion_arrow
    • variations