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

• Denotational semantics for guarded dependent type theory
  Aleš Bizjak and Rasmus Ejlers Møgelberg
  Mathematical Strucures in Computer Science, Vol 30, Issue 4
  ArXiv preprint

• Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
  Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
  POPL 2019
  Preprint and Coq formalization

• Guarded Cubical Type Theory
  Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi
  Journal of Automated Reasoning, Special Issue on Homotopy Type Theory and Univalent Foundations, 2018 (extended version of the CSL’16 paper)
  ArXiv preprint

• A Model of Guarded Recursion via Generalised Equilogical Spaces
  Aleš Bizjak and Lars Birkedal
  TCS
  PDF (preprint)

• Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
  Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak, Marco Gaboardi, and Deepak Garg
  ESOP 2018
  ArXiv preprint

• Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic
  Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer
  JFP
  PDF (preprint)

• On Models of Higher-Order Separation Logic
  Aleš Bizjak and Lars Birkedal
  MFPS 2017
  Preprint

• The Essence of Higher-Order Concurrent Separation Logic
  Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal
  ESOP 2017
  Preprint

• Guarded Cubical Type Theory: Path Equality for Guarded Recursion
  Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi
  CSL 2016
  ArXiv preprint

• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
  Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal
  Logical Methods in Computer Science special issue (journal version of FoSSaCS’15 paper).
  ArXiv

• Guarded Dependent Type Theory with Coinductive Types
  Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Rasmus Ejlers Møgelberg, and Lars Birkedal
  FoSSaCS 2016
  ArXiv preprint

• ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages
  Filip Sieczkowski, Aleš Bizjak, and Lars Birkedal
  ITP 2015
  Preprint

• A model of guarded recursion with clock synchronisation
  Aleš Bizjak and Rasmus Ejlers Møgelberg
  MFPS 2015

• Step-Indexed Logical Relations for Probability
  Aleš Bizjak and Lars Birkedal
  FoSSaCS 2015
  ArXiv preprint

• Programming and Reasoning with Guarded Recursion for Coinductive Types
  Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal
  FoSSaCS 2015
  ArXiv preprint

• A Model of Countable Nondeterminism in Guarded Type Theory
  Aleš Bizjak, Lars Birkedal, and Marino Miculan
  RTA-TLCA 2014
  Preprint | Technical report

• Step-Indexed Relational Reasoning for Countable Nondeterminism
  Lars Birkedal, Aleš Bizjak, and Jan Schwinghammer
  Logical Methods in Computer Science, Volume 9, Issue 4, 2013
  ArXiv preprint

PhD thesis

• On Semantics and Applications of Guarded Recursion
  Aarhus University, 2016

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

Service

• POPL 2019 artifact evaluation committee member

• HOPE 2018 program committee member

• ICFP 2018 artifact evaluation committee member

• MFPS 2018 program committee member

• LMCS layout editor

• POPL 2018 artifact evaluation committee member

• POPL 2017 artifact evaluation committee member

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.