lukaszcz

compiler construction, programming language design, proof automation, computational logic

Pinned Repositories

asm32
An educational assembler for a subset of 32bit x86 instructions.
Language:C1 2 00
clc
Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.
Language:Coq1 2 00
coinduction
A Coq plugin to help with proofs by coinduction.
Language:OCaml9 4 00
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.
Language:Coq6 5 01
coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Language:OCaml208 8 8531
hcpl
A prototypical proof checker and programming language based on illative combinatory logic
Language:OCaml0 2 00
infinitary-confluence
Formalisation of a coinductive confluence proof for the infinitary lambda calculus.
Language:Coq8 2 00
javalette
An educational compiler for Javalette, written in C
Language:C2 3 00
sortalgs
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Language:Coq1 1 00
tptp2coq
Conversion of the FOF TPTP format to Coq files
Language:Haskell4 2 01

lukaszcz's Repositories

lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Language:OCaml208 8 8531
lukaszcz/coinduction
A Coq plugin to help with proofs by coinduction.
Language:OCaml9 4 00
lukaszcz/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.
Language:Coq6 5 01
lukaszcz/tptp2coq
Conversion of the FOF TPTP format to Coq files
Language:Haskell4 2 01
lukaszcz/javalette
An educational compiler for Javalette, written in C
Language:C2 3 00
lukaszcz/asm32
An educational assembler for a subset of 32bit x86 instructions.
Language:C1 2 00
lukaszcz/cfoprover
An experimental connection-driven prover for intuitionistic first-order logic
Language:Haskell1 2 00
lukaszcz/lukaszcz.github.io
Language:HTML1 2 01
lukaszcz/pascaladt
A library of algorithms and data structures for the Free Pascal Compiler.
Language:Pascal1 2 0
lukaszcz/ramsey
Proof of the finite Ramsey's theorem.
Language:Coq1 2 0
lukaszcz/sortalgs
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Language:Coq1 1 00
lukaszcz/hcpl
A prototypical proof checker and programming language based on illative combinatory logic
Language:OCaml0 2 00
lukaszcz/bst
Binary Search Trees in Coq
Language:Coq2 0
lukaszcz/cmakefile
Automatic build system for C and C++.
Language:Makefile2 0
lukaszcz/cosmwasmtest
Language:Rust1 0
lukaszcz/diaconescu
Formalisation of two variants of Diaconescu's theorem
Language:Coq2 0
lukaszcz/dict2
A dictionary viewing application for Linux.
Language:C2 0
lukaszcz/eval-compcert
CoqHammer evaluation results on CompCert
2 0
lukaszcz/gram
Language:Haskell2 0
lukaszcz/hexcalc
A calculator which lets you see the results of various x86 instructions. Written in x86 assembly.
Language:Assembly2 0
lukaszcz/juvix-docs
Juvix Official Documentation
Language:Makefile0 0
lukaszcz/lukaszcz
1 0
lukaszcz/mcp
A simple macro processor.
Language:C2 0
lukaszcz/minijuvix
A functional language for writing validity predicates
Language:Haskell0 0
lukaszcz/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Language:OCaml1 0
lukaszcz/smtcoq
Communication between Coq and SAT/SMT solvers
Language:Coq1 0
lukaszcz/snake
A snake game for Linux written in x86 assembly.
Language:Assembly2 0
lukaszcz/spike-prover
Automatically exported from code.google.com/p/spike-prover
Language:Coq1 0
lukaszcz/srcdoc
Documentation generator a la doxygen for Free Pascal and Delphi.
Language:Pascal2 0
lukaszcz/vamp-ir
Vamp-IR is a proof-system-agnostic language for writing arithmetic circuits
Language:Rust0 0