Formalizations

Below is an incomplete list of Coq formalisations I’ve written over the years.

• A coinductive confluence proof for the infinitary lambda calculus: A formalisation of my paper about the infinitary lambda calculus.
• Confluence of an extension of Combinatory Logic by boolean constants: A formalisation of my paper which solves open problem 15 from the RTA list of open problems.
• Concrete semantics with Coq and CoqHammer: A re-formalisation in Coq of several chapters from the book “Concrete Semantics with Isabelle/HOL”. The formalisation concerns operational semantics and compilation correctness for a simple imperative language. In cooperation with Burak Ekici and Cezary Kaliszyk.
• Sorting algorithms: quick sort, merge sort, insertion sort, selection sort.
• Binary search trees.
• Diaconescu’s theorem.
• Finite Ramsey’s theorem.