Juvix: A functional programming language for intent-centric declarative decentralized applications.

CoqHammer: An automated reasoning hammer tool for Coq - proof automation for dependent type theory.

Lean2RISC0: Cross-compiling Lean 4 to the RISC Zero zkVM.

Coinduction: A Coq plugin to help with proofs by coinduction.

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

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.

PascalAdt: A library of algorithms and data structures for the Free Pascal Compiler.

SrcDoc: Documentation generator a la doxygen for Free Pascal and Delphi.