GeoCoqCoq Logo

Toward a Certified Encyclopedia of Triangle CentersCoq Logo

GeoProof Nominal Logo

The Area Method Coq Logo

Projective Geometry (including Desargues' theorem using ranks) Coq Logo

Projective geometry in Coq (also available as a .tar.gz compatible with Coq v8.3).

Abstract Rewriting Coq Logo

Logical Relations Nominal Logo

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 ProofsNominal Logo

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".