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