TAPL-Coq

Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages.

Name		Name	Last commit message	Last commit date
Latest commit History 196 Commits
.gitignore		.gitignore
Damas-Milner.v		Damas-Milner.v
Exception-STLC.v		Exception-STLC.v
Hindley-Milner.v		Hindley-Milner.v
Mini-Ext-STLC.v		Mini-Ext-STLC.v
OrderedRecSubtyping-STLC.v		OrderedRecSubtyping-STLC.v
Patterns.v		Patterns.v
README.md		README.md
Ref-STLC.v		Ref-STLC.v
STLC.v		STLC.v
Subsumption-STLC.v		Subsumption-STLC.v
System-F.v		System-F.v

Provide feedback