In this repository are my solutions to the exercises in software foundations coq tutorial.
- Preface
- Basics: Functional Programming in Coq
- Induction: Proof by Induction
- Lists: Working with Structured Data
- Poly: Polymorphism and Higher-Order Functions
- MoreCoq: More About Coq
- Logic: Logic in Coq
- Prop: Propositions and Evidence
- MoreLogic
- ProofObjects: Working with Explicit Evidence in Coq
- MoreInd: More on Induction
- SfLib: Software Foundations Library
- Imp: Simple Imperative Programs
- ImpParser: Lexing and Parsing in Coq
- ImpCEvalFun: Evaluation Function for Imp
- Extraction: Extracting ML from Coq
- Equiv: Program Equivalence
- Hoare: Hoare Logic, Part I
- Hoare2: Hoare Logic, Part II
- Smallstep: Small-step Operational Semantics
- Auto: More Automation
- Types: Type Systems
- Stlc: The Simply Typed Lambda-Calculus
- StlcProp: Properties of STLC
- MoreStlc: More on the Simply Typed Lambda-Calculus
- Sub: Subtyping