Software Foundations

Volume 1: Logical Foundations

• Software Foundation : Logical Foundation

Current Progress

• Functional Programming in Coq (Basics)
• Proof by Induction (Induction)
• Working with Structured Data (Lists)
• Polymorphism and Higher-Order Functions (Poly)
• More Basic Tactics (Tactics)
• Logic in Coq (Logic)
• Inductively Defined Propositions (IndProp)
• Total and Partial Maps (Maps)
• The Curry-Howard Correspondence (ProofObjects)
• Induction Principles (IndPrinciples)
• Properties of Relations (Rel)
• Simple Imperative Programs (Imp)
• Lexing and Parsing in Coq (ImpParser)
• An Evaluation Function for Imp (ImpCEvalFun)
• Extracting ML from Coq (Extraction)
• More Automation (Auto)
• Postscript