Software

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. Written in OCaml.
• 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.
• MCP: A macro processor.
• 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++.