Below is an incomplete list of open source software I’ve written over the years. The projects range from small programs with several hundred lines to medium-sized projects of 10k-30k lines. Some are in a prototype stage, but all have been tested, debugged and completed enough for at least basic usability.

  • 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.
  • PascalAdt: A library of data structures and algorithms for the Free Pascal compiler.
  • Javalette: An educational compiler for Javalette - a subset of C without pointers and dynamic memory allocation.
  • ASM32: An educational assembler for a subset of 32bit x86 instructions. Produces Linux ELF executables.
  • MCP: A macro processor.
  • 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.
  • Snake: A snake game for Linux written in x86 assembly.
  • CMakefile: An automatic build system for C/C++.