Formalizations

Below is an incomplete list of Coq formalisations I’ve written over the years. These range from small formalisations with several hundred lines to bigger projects with thousands of lines formalising entire papers.

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