I am currently a software engineer. Previously I was a postdoctoral researcher at the Department of Computer Science of Aarhus University where I worked on program logics for concurrency, and semantics of programming languages, logics, and type theories.

Google Scholar | DBLP | Github

Publications

PhD thesis

Notes and tutorials

Service

Software

Occasionally I write some software, some of which you might find useful, hence I list it here. My Github account is here.

Alg, a program for enumerating models of algebraic theories

Alg is a program for enumeration of finite models of single-sorted first-order theories. Such a theory is given by a signature (a list of constants, operations and relations) and axioms expressed in first-order logic. Examples of first-order theories include groups, lattices, rings, fields, posets, graphs, and many others. Alg can do the following:

Written together with Andrej Bauer. The source is on Github and we have also written a manual.

A Turing machine simulator

A very simple Turing machine simulator written for use in a course for second year undergraduate students. Written in Haskell and compiled to Javascript with the Haste compiler.

Here you can see it running. The source is available on Bitbucket.

Another Turing machine simulator and compiler

A more sophisticated Turing machine simulator with a proper parser and syntax for defining them. It also allows writing multi-tape Turing machines and running them. Part of the project is also a compiler from a simple variant of call-by-value λ-calculus to 5-tape Turing machines with a few examples showing how the compiled Turing machine computes the given function.

The source, with examples and more details, is on Bitbucket.