This is a collection of software I’ve written that is available for download, mostly programming language implementations and related tools.
- Idris, a functional programming language with dependent types. Idris is a research project to create a dependently typed programming language suitable for systems programming – the emphasis is therefore on producing good compiled code and a convenient programming notation.
- Ivor, a proof engine. Ivor is a Haskell library which provides a dependent type theory and a tactic based theorem proving engine. It is primarily used by Idris for type checking and proof scripts.
- Epic, a library for generating compilers. Epic (the name derives from Epigram Compiler) is a compiler for a small functional language, intended as a reusable back end for high level functional languages. It is currently used as the back end for Idris as well as an experimental back end for Agda. It is ultimately intended for use by Epigram.
- Kaya, a mostly-imperative language with static types, which is an attempt to bring some functional language features (especially algebraic data types and type inference) into a more accessible imperative language. I started writing this a few years ago mostly as an exercise in seeing-if-I-could but with the help of Durham University Computing Society it evolved into something quite useful, and I believe a few of them do use it. I don’t actively maintain it much any more, but I think with some clean up of syntax and more disciplined overloading it could be pretty useful.
- Whitespace speaks for itself, or more precisely, doesn’t.
- This LaTeX thesis document class for Durham University might still be useful to someone somewhere. It should also be easy to modify for use for other universities’ thesis guidelines.
- There is also this unusual method for computing pi that I wrote while an undergraduate, and no doubt meant to be doing something else…