Julien Narboux

An automated theorem prover based on Coherent Logic. Larus can generate readable and machine checkable proofs (joint work with Predrag Janicic).

Some geometry theorems formalized in Coq using Tarski's axiom system (joint work with Pierre Boutry and Gabriel Braun). The library has been ported to Isabelle by Roland Coghetto.

Thousands of properties of triangle centers (joint work with David Braun).

An interactive geometry software with proof related features (online demo) .

A decision procedure for euclidean geometry in Coq.

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

Some proofs in the theory of abstract rewriting using a diagrammatic approach.

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

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