Skip to content

yhuang912/software-foundations

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

62 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Software Foundations

These files contain my solutions to the exercises found in the Software Foundations online course.

TODO

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

About

Solutions to the Software Foundations online course

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Coq 100.0%