Engineering Formal Metatheory

The paper: Engineering Formal Metatheory
by Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack and Stephanie Weirich.
In the proceedings of POPL'08.

[NEW] A working version of the library that compiles with CoqV8.2 is available from here.
It is still incomplete at this time, but an official release should be ready for April 2009.
Please don't hesitate to contact me if you encounter any difficulty while using this library.
Note: the documentation for the extended set of tactics (file LibTactics.v) can be found on this page

The corresponding Coq proof scripts are available for download.
You may also browse the documentation directly from the tables below.

Language	Formalized	Highlighted Source	CoqDoc Generated
System-Fsub (PoplMark 1A+2A)	Type soundness	Fsub_Definitions Fsub_Infrastructure Fsub_Soundness	Fsub_Definitions Fsub_Infrastructure Fsub_Soundness
ML with datatypes, recursion, references and exceptions	Type soundness	ML_Definitions ML_Infrastructure ML_Soundness	ML_Definitions ML_Infrastructure ML_Soundness
Pure lambda calculus	Church-Rosser	Lambda_Definitions Lambda_Infrastructure Lambda_ChurchRosser	Lambda_Definitions Lambda_Infrastructure Lambda_ChurchRosser
Calculus of Constructions	Subject reduction	CoC_Definitions CoC_Infrastructure CoC_BetaStar CoC_ChurchRosser CoC_Conversion CoC_Preservation	CoC_Definitions CoC_Infrastructure CoC_BetaStar CoC_ChurchRosser CoC_Conversion CoC_Preservation
Generic Libraries	-	Lib_Tactic Metatheory_Var Metatheory_Fresh Metatheory_Env Metatheory	Lib_Tactic Metatheory_Var Metatheory_Fresh Metatheory_Env Metatheory

For pedagogical purposes, we also provide with a collection of simpler developments.

Language	Formalized	Highlighted Source	CoqDoc Generated
STLC	Type soundness	STLC_Core_Definitions STLC_Core_Infrastructure STLC_Core_Soundness	STLC_Core_Definitions STLC_Core_Infrastructure STLC_Core_Soundness
STLC, extra Material	Adequacy, Full-beta-reduction, Light development	STLC_Core_Adequacy STLC_Core_FullBeta STLC_Core_Light	STLC_Core_Adequacy STLC_Core_FullBeta STLC_Core_Light
STLC + Datatypes	Type soundness	STLC_Data_Definitions STLC_Data_Infrastructure STLC_Data_Soundness	STLC_Data_Definitions STLC_Data_Infrastructure STLC_Data_Soundness
STLC + Exceptions	Type soundness	STLC_Exn_Definitions STLC_Exn_Infrastructure STLC_Exn_Soundness	STLC_Exn_Definitions STLC_Exn_Infrastructure STLC_Exn_Soundness
STLC + References	Type soundness	STLC_Ref_Definitions STLC_Ref_Infrastructure STLC_Ref_Soundness	STLC_Ref_Definitions STLC_Ref_Infrastructure STLC_Ref_Soundness
STLC with annotations	Decidability of type-checking	STLC_Dec_Definitions STLC_Dec_Infrastructure STLC_Dec_Soundness STLC_Dec_Decidability	STLC_Dec_Definitions STLC_Dec_Infrastructure STLC_Dec_Soundness STLC_Dec_Decidability
Mini-ML (core only)	Type soundness	ML_Core_Definitions ML_Core_Infrastructure ML_Core_Soundness	ML_Core_Definitions ML_Core_Infrastructure ML_Core_Soundness