Toward a Certified Encyclopedia of Triangle Centers
The Area Method
Projective Geometry (including Desargues' theorem using ranks)
A formalisation of the chapter on logical relations by Karl Crary of the book "Advanced Topics in Types and Programming Languages" (joint work with Christian Urban).
The documented proof generated from the Isabelle file (.pdf) and the original Isabelle file is here: .thy, new versions are distributed with the Isabelle proof assistant in the directory "src/HOL/Nominal/Examples".
Nominal Formalisations of Typical SOS Proofs
We present a formalisation using the nominal package of a few properties of the simply typed lambda calculus extended with product and some types. This includes proofs of subject reduction property, the weakening lemma, the type substitution lemma, and the termination of evaluation expressed by a big step semantic (joint work with Christian Urban).
The paper (.pdf), the Isabelle file is now distributed within the Isabelle proof assistant in the directory "src/HOL/Nominal/Examples".