-
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.
lukaszcz
More
compiler construction, programming language design, proof automation, computational logic
Block or Report
Block or report lukaszcz
Report abuse
Contact GitHub support about this user’s behavior. Learn more about reporting abuse.
Report abuse