Larus
GeoCoq
Toward a Certified Encyclopedia of Triangle Centers
The Area Method 
Projective Geometry (including Desargues' theorem using ranks) 
Projective geometry in Coq (also available as a .tar.gz compatible with Coq v8.3). This development has been ported to Isabelle by Anthony Bordg (link).
Logical Relations 
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 (.pdf) is now distributed within the Isabelle proof assistant in the directory "src/HOL/Nominal/Examples".