Skip to content
View lukaszcz's full-sized avatar
Block or Report

Block or report lukaszcz

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
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.

  • 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's activity is private