-
CoqHammer: An automated reasoning hammer tool for Coq - proof automation for dependent type theory.
-
Coinduction: A Coq plugin to help with proofs by coinduction.
-
HCPL: A prototypical proof checker and programming language based on illative combinatory logic.
-
Javalette: An educational compiler for Javalette, written in C.
-
CMakefile: Automatic build system for C and C++.
-
COQ-IMP: Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL".
-
CLC: Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.
-
infinitary-confluence: Formalisation of a coinductive confluence proof for the infinitary lambda calculus.
-
sortalgs: Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
-
BST: Binary Search Trees in Coq.
-
Diaconescu: Formalisation of two variants of Diaconescu's theorem.
-
tptp2coq: Conversion of the FOF TPTP format to Coq files.
-
tptp2ileancop: Run ileancop on the ILTP library.
More
compiler construction, programming language design, proof automation, computational logic