These files contain my solutions to the exercises found in the Software Foundations online course.
Current progress:
- 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
- Review1: Review Session for First Midterm
- 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
- Rel: Binary relations
- Hoare: Hoare Logic, Part I
- Hoare2: Hoare Logic, Part II
- HoareAsLogic: Hoare as Logic
- Smallstep: Small-step Operational Semantics
- References: Typing Mutable References
- Review2: Review Session for Second Midterm
- Auto: More Automation
- UseAuto: More Automation
- LibTactics: Tactics Library
- UseTactics: More Automation
- Types: Type Systems
- Typechecking: Type Checking
- Symbols: Symbols
- Stlc: The Simply Typed Lambda-Calculus
- StlcProp: Properties of STLC
- MoreStlc: More on the Simply Typed Lambda-Calculus
- Records: Adding Records to STLC
- Sub: Subtyping
- RecordSub: Subtyping with Records
- Norm: Normalization
- PE: Partial Evaluations
- Postscript: Postscript