lukaszcz / smtcoq Goto Github PK

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.