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.