Dominique Larchey-Wendling

ite-normalisation. L. Paulson's If-Then-Else normalisation algorithm in Coq via simulated Induction-Recursion

Introduction-to-Coq. Introduction to the Coq proof assistant

The-Braga-Method. The Braga Method for Extracting Certified OCaml from Coq code

Coq-Phase-Semantics. Coq Source for Relational Phase Semantics and Cut-elimination

Hilbert-Basis-Theorem. Hilbert Basis Theorem in Coq/Rocq

Coq-is-total. A proof that Coq contains any total mu-recursive function

PC19. Exercices and Examples for the PC'19 Autumn school

Mso. The well-foundedness of the multiset ordering

Ramsey. Ramsey's theorem in Type Theory and applications

Kruskal-Trees. Coq library for rose trees

Accessibility. A small course on the inductive accessibility predicate in Coq

BFE. Certification of Breadth-First algorithms by Extraction

Murec_Extraction. Extraction of µ-recursive algorithms in Coq

Kruskal-Fan. The Fan theorem for inductive bars and a constructive variant of König's lemma

Kruskal-Theorems. Kruskal and Higman type tree theorems for the Kruskal-AlmostFull library

Hydra. Hercules kills the Hydra in Coq

Karp-Miller. A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull

wf-strict-order-finite. Direct proof that strict orders on listable types are well-founded

Kruskal-AlmostFull. Library of basic results about Almost Full relations in Coq

Quasi-Morphisms. Quasi morphisms for Almost Full relations

The-Tortoise-and-the-Hare. The Tortoise and the Hare in Coq. Constructive extraction via Bar inductive predicates (see README.md below).

Combinatory-Logic-for-students. Confluence de la logique combinatoire en Coq

Tree-mirror. Tree mirroring specified in a small fun. language and Coq proofs of correctedness