Pinned

1. coqhammer Public

   CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

   OCaml 186 25

2. hcpl Public

   A prototypical proof checker and programming language based on illative combinatory logic

   OCaml

3. coinduction Public

   A Coq plugin to help with proofs by coinduction.

   OCaml 5

4. sortalgs Public

   Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.

   Coq

5. clc Public

   Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.

   Coq 1

6. infinitary-confluence Public

   Formalisation of a coinductive confluence proof for the infinitary lambda calculus.

   Coq 8