Toggle navigation
Hux Blog
Home
About
Archive
Archive
keep hungry keep foolish
Show All
35
笔记
35
软件基础 SF
35
Coq
35
2019
「软件基础 - PLF」 19. Partial Evaluation
「软件基础 - PLF」 18. Theory And Practice Of Automation In Coq Proofs
「软件基础 - PLF」 17. Tactic Library For Coq: A Gentle Introduction
「软件基础 - PLF」 16. A Collection of Handy General-Purpose Tactics
「软件基础 - PLF」 15. Normalization of STLC
「软件基础 - PLF」 14. Subtyping with Records
「软件基础 - PLF」 13. Typing Mutable References
「软件基础 - PLF」 12. Adding Records To STLC
「软件基础 - PLF」 11. TypeChecking
「软件基础 - PLF」 10. Subtyping
「软件基础 - PLF」 9. More on STLC
「软件基础 - PLF」 8. Properties of STLC
「软件基础 - PLF」 7. The Simply Typed Lambda-Calculus
「软件基础 - PLF」 6. Type Systems
「软件基础 - PLF」 5. Small-Step Operational Semantics
「软件基础 - PLF」 4. Hoare Logic as a Logic
「软件基础 - PLF」 3. Hoare Logic, Part II
「软件基础 - PLF」 2. Hoare Logic, Part I
「软件基础 - PLF」 1. Program Equivalence 程序的等价关系
「软件基础 - LF」 16. More Automation
「软件基础 - LF」 15. Extracting ML From Coq
「软件基础 - LF」 14. An Evaluation Function For Imp
「软件基础 - LF」 13. Lexing And Parsing In Coq
「软件基础 - LF」 12. IMP
「软件基础 - LF」 11. Rel - properties of relations
「软件基础 - LF」 10. Induction Principles
「软件基础 - LF」 9. Proof Objects - The Curry-Howard Correspondence
「软件基础 - LF」 8. Maps - Total and Partial Maps
「软件基础 - LF」 7. Ind Prop (归纳定义命题)
「软件基础 - LF」 6. Logic
「软件基础 - LF」 5. Tactics
「软件基础 - LF」 4. Poly
「软件基础 - LF」 3. List
「软件基础 - LF」 2. Induction
「软件基础 - LF」 1. Basics (FP in Coq)
