Łukasz Czajka

compiler engineer, programming language designer, proof automation specialist, researcher in computational logic

Below is an incomplete list of open source software I’ve written by myself or significantly contributed to over the years.

  • Juvix: A functional language for declarative decentralized applications. I was one of the main developers.
  • CoqHammer: An automated reasoning system for Coq. In cooperation with Cezary Kaliszyk.
  • Coinduction: A Coq plugin which helps with proofs by coinduction.
  • HCPL: A prototypical proof checker and programming language based on illative combinatory logic. Written in OCaml.
  • Lean2RISC0: Cross-compiling Lean 4 to the RISC Zero zkVM.
  • Javalette: An educational compiler for Javalette - a subset of C without pointers and dynamic memory allocation. Written in C.
  • ASM32: An educational assembler for a subset of 32bit x86 instructions. Produces Linux ELF executables. Written in C.
  • PascalAdt: A library of data structures and algorithms for the Free Pascal compiler.
  • Dict2: A dictionary viewing application for Linux.
  • SrcDoc: A documentation generator a la Doxygen for Free Pascal and Delphi.
  • HexCalc: A calculator which lets you see the results of various x86 instructions. Written in x86 assembly.
  • CMakefile: An automatic build system for C/C++.