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