I am a postdoctoral researcher at the Department of Computer Science of Aarhus University. I work on program logics for concurrency, and semantics of programming languages, logics, and type theories.
Google Scholar  DBLP  Pure
Drafts
 Denotational semantics for guarded dependent type theory
Aleš Bizjak and Rasmus Ejlers Møgelberg
Manuscript
ArXiv preprint
Publications

Iron: Managing Obligations in HigherOrder 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 HigherOrder Concurrent Separation Logic
Ralf Jung, Robbert Krebbers, JacquesHenri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer
JFP
PDF (preprint) 
On Models of HigherOrder Separation Logic
Aleš Bizjak and Lars Birkedal
MFPS 2017
Preprint 
The Essence of HigherOrder Concurrent Separation Logic
Robbert Krebbers, Ralf Jung, Aleš Bizjak, JacquesHenri 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 LambdaCalculus: 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 HigherOrder 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 
StepIndexed 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
RTATLCA 2014
Preprint  Technical report 
StepIndexed 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 stepindexed 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 Bitbucket account is here, and my Github account is here.
Alg, a program for enumerating models of algebraic theories
Alg is a program for enumeration of finite models of singlesorted firstorder theories. Such a theory is given by a signature (a list of constants, operations and relations) and axioms expressed in firstorder logic. Examples of firstorder theories include groups, lattices, rings, fields, posets, graphs, and many others. Alg can do the following:
 list or count all nonisomorphic models of a given theory,
 list or count all nonisomorphic 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 multitape Turing machines and running them. Part of the project is also a compiler from a simple variant of callbyvalue λcalculus to 5tape 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.