From POPLmark

• Page with Coq tips from the coq-club mailing list and other sources.

• An annotated bibliography that contains a list of contributions related to formalization of lambda-calculus and type theory.

• Variable binding

• Tutorials

• Comparative proofs of the soundness of Featherweight Java:
  • By Stephanie Weirich, using Coq : [fj-coq.tar.gz]
  • By Stephanie Weirich and Geoffrey Washburn, using Twelf : [fj-twelf.tar.gz]
  • By Nate Foster and Dimitris Vytiniotis, using Isabelle/HOL : [FJ.tar.gz]
• [baydemir-stlc.tar.gz]: A proof in Coq of type soundness for the simply-typed lambda calculus. Uses de Bruijn indices to encode binding. Author: Brian E. Aydemir.
• Quite a few results of simply-typed lambda calculus encoded with de Bruijn indices, including subject reduction, are part of the Isabelle distribution. Documentation is also available online: http://isabelle.in.tum.de/library/HOL/Lambda/index.html.
• Jinja is a Java-like language designed to exhibit core features of the Java language architecture. Its formalization in Isabelle/HOL provides a unified model of the source langage, virtual machine, and compiler.
• Comparison by Xavier Leroy and Andrew Appel: A list-machine benchmark for mechanized metatheory. Results summarized in a technical report.

[edit] Theorem provers and proof assistants

• Systems: ACL2, Coq, HOL, HOL Light, Isabelle, MetaPRL, PVS, Twelf, Matita
• Systems of historical interest: LEGO, NuPRL