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

# Notes and tutorials

• Some theorems about mutually recursive domain equations in the category of preordered COFEs Aleš Bizjak
PDF

• A Taste of Categorical Logic - Tutorial Notes
Aleš Bizjak and Lars Birkedal
PDF

• A note on the transitivity of step-indexed logical relations
Lars Birkedal and Aleš Bizjak
PDF

# 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:

• list or count all non-isomorphic models of a given theory,
• list or count all non-isomorphic indecomposable models of a given theory.

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.