DOWNLOAD HYBRID
The Hybrid package has been developed for Coq and Isabelle/HOL:
- A tar file for Coq
version 8.0pl3 is here.
This contains the subject reduction example for the simply typed lambda
calculus.
- Hybrid.thy for Isabelle/HOL version 2011.
(older versions)
For an extended example in Isabelle/HOL version 2008, see Alan Martin's
case study:
Five formalizations of evaluation, typing, and subject reduction
for Mini-ML with references.