Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
My solutions to the exercises in 'Software Foundations'
Coq OCaml
branch: master


latest commit aff2764560
@timjb authored
Failed to load latest commit information.
.depend unpacked .tar.gz from
.gitignore removed web contents
Basics.v finished chapter 1
Equiv.v finished Equiv.v
Extraction.v unpacked .tar.gz from
Extraction2.v unpacked .tar.gz from
Gen.v finished fourth chapter (Gen.v)
Hoare.v finished Hoare.v
HoareAsLogic.v finished HoareAsLogic.v
HoareList.v finished HoareList.v
Imp.v finished Imp.v
ImpCEvalFun.v finished ImpCEvalFun.v
ImpParser.v unpacked .tar.gz from
LICENSE unpacked .tar.gz from
LibTactics.v corrected LibTactics.v; finished UseTactics.v
Lists.v finished second chapter
Logic.v prove 5 characterizations of classical logic equivalent
Makefile unpacked .tar.gz from
MoreStlc.v added a fixpoint operator to the simply typed lambda calculus in More…
Norm.v finished Norm.v (normalisation of the simply typed lambda calculus)
NormInType.v unpacked .tar.gz from
PE.v unpacked .tar.gz from
Poly.v finished third chapter (Poly.v)
Postscript.v unpacked .tar.gz from
Preface.v unpacked .tar.gz from
Prop.v finished fifth chapter (Prop.v) added
RecordSub.v finished RecordSub.v
Records.v finished Records.v
References.v finished References.v
Rel.v finished Rel.v
SfLib.v unpacked .tar.gz from
Smallstep.v finished Smallstep
Stlc.v finished Stlc.v (simply typed lambda calculus)
Sub.v finished Subtyping chapter (Sub.v)
Symbols.v unpacked .tar.gz from
Typechecking.v unpacked .tar.gz from
Types.v finished Types.v
UseAuto.v UseAuto.v
UseTactics.v corrected LibTactics.v; finished UseTactics.v unpacked .tar.gz from unpacked .tar.gz from
imp.mli unpacked .tar.gz from unpacked .tar.gz from
imp1.mli unpacked .tar.gz from unpacked .tar.gz from
imp2.mli unpacked .tar.gz from unpacked .tar.gz from unpacked .tar.gz from
norm.mli unpacked .tar.gz from unpacked .tar.gz from

Software foundations

This repository contains a copy of of Software Foundations extended with my solutions to the exercises. You can use it's contents (both the original text and my code) under the terms of the MIT license.

Something went wrong with that request. Please try again.