Łukasz Czajka

coqhammer. CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

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

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

srcdoc. Documentation generator a la doxygen for Free Pascal and Delphi.

COQ-IMP. Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL". Formalized using a now outdated version of CoqHammer.

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

tptp2coq. Conversion of the FOF TPTP format to Coq files

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

javalette. An educational compiler for Javalette, written in C

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

asm32. An educational assembler for a subset of 32bit x86 instructions.

ramsey. Proof of the finite Ramsey's theorem.

cfoprover. An experimental connection-driven prover for intuitionistic first-order logic

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

bst. Binary Search Trees in Coq

mcp. A simple macro processor.