Step-Indexed Relational Reasoning for Countable Nondeterminism. - Lars Birkedal; Ales Bizjak; Jan Schwinghammer (Log. Methods Comput. Sci., 2013)

A Model of Countable Nondeterminism in Guarded Type Theory. - Ales Bizjak; Lars Birkedal; Marino Miculan (RTA-TLCA, 2014)

Step-Indexed Logical Relations for Probability. - Ales Bizjak; Lars Birkedal (FoSSaCS, 2015)

Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (FoSSaCS, 2015)

ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. - Filip Sieczkowski; Ales Bizjak; Lars Birkedal (ITP, 2015)

Step-Indexed Logical Relations for Probability (long version). - Ales Bizjak; Lars Birkedal (CoRR, 2015)

A Model of Guarded Recursion With Clock Synchronisation. - Ales Bizjak; Rasmus Ejlers Møgelberg (MFPS, 2015)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (CSL, 2016)

Guarded Dependent Type Theory with Coinductive Types. - Ales Bizjak; Hans Bugge Grathwohl; Ranald Clouston; Rasmus Ejlers Møgelberg; Lars Birkedal (FoSSaCS, 2016)

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (Log. Methods Comput. Sci., 2016)

The Essence of Higher-Order Concurrent Separation Logic. - Robbert Krebbers; Ralf Jung 002; Ales Bizjak; Jacques-Henri Jourdan; Derek Dreyer; Lars Birkedal (ESOP, 2017)

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. - Alejandro Aguirre 001; Gilles Barthe; Lars Birkedal; Ales Bizjak; Marco Gaboardi; Deepak Garg 001 (ESOP, 2018)

On Models of Higher-Order Separation Logic. - Ales Bizjak; Lars Birkedal (MFPS, 2018)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic. - Ralf Jung 002; Robbert Krebbers; Jacques-Henri Jourdan; Ales Bizjak; Lars Birkedal; Derek Dreyer (J. Funct. Program., 2018)

A model of guarded recursion via generalised equilogical spaces. - Ales Bizjak; Lars Birkedal (Theor. Comput. Sci., 2018)

Guarded Cubical Type Theory. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (J. Autom. Reason., 2019)

Iron: managing obligations in higher-order concurrent separation logic. - Ales Bizjak; Daniel Gratzer; Robbert Krebbers; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Denotational semantics for guarded dependent type theory. - Ales Bizjak; Rasmus Ejlers Møgelberg (Math. Struct. Comput. Sci., 2020)