Skip to content
View lukaszcz's full-sized avatar

Block or report lukaszcz

Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
lukaszcz/README.md

  • 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.

  • ASM32: An educational assembler for a subset of 32-bit x86 instructions.

  • 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.

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

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

@lukaszcz's activity is private