Skip to content
View lukaszcz's full-sized avatar
39 followers · 0 following

Achievements

Achievement: Arctic Code Vault Contributor

Achievements

Achievement: Arctic Code Vault Contributor

Block or report lukaszcz

Report abuse

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

Report abuse
lukaszcz/README.md

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

Pinned Loading

  1. coqhammer coqhammer Public

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

    OCaml 239 36

  2. hcpl hcpl Public

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

    OCaml 5 1

  3. coinduction coinduction Public

    A Coq plugin to help with proofs by coinduction.

    OCaml 10

  4. sortalgs sortalgs Public

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

    Coq 2

  5. clc clc Public

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

    Coq 1

  6. infinitary-confluence infinitary-confluence Public

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

    Coq 8