Ales Bizjak

Publication Activity (10 Years)

Years Active: 2013-2020
Publications (10 Years): 16

Top Topics

Lambda Calculus

Reasoning Systems

Programming Language

Top Venues

Log. Methods Comput. Sci.

Publications

Ales Bizjak, Rasmus Ejlers Møgelberg
Denotational semantics for guarded dependent type theory. Math. Struct. Comput. Sci. 30 (4) (2020)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. J. Autom. Reason. 63 (2) (2019)
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
Iron: managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3 (POPL) (2019)
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)
Ales Bizjak, Lars Birkedal
A model of guarded recursion via generalised equilogical spaces. Theor. Comput. Sci. 722 (2018)
Ales Bizjak, Rasmus Ejlers Møgelberg
Denotational semantics for guarded dependent type theory. CoRR (2018)
Ales Bizjak, Lars Birkedal
On Models of Higher-Order Separation Logic. MFPS (2018)
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. CoRR (2018)
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. ESOP (2018)
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
The Essence of Higher-Order Concurrent Separation Logic. ESOP (2017)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CSL (2016)
Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal
Guarded Dependent Type Theory with Coinductive Types. CoRR (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CoRR (2016)
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Log. Methods Comput. Sci. 12 (3) (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. CoRR (2016)
Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal
Guarded Dependent Type Theory with Coinductive Types. FoSSaCS (2016)
Filip Sieczkowski, Ales Bizjak, Lars Birkedal
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. ITP (2015)
Ales Bizjak, Lars Birkedal
Step-Indexed Logical Relations for Probability. FoSSaCS (2015)
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS (2015)
Ales Bizjak, Rasmus Ejlers Møgelberg
A Model of Guarded Recursion With Clock Synchronisation. MFPS (2015)
Ales Bizjak, Lars Birkedal
Step-Indexed Logical Relations for Probability (long version). CoRR (2015)
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
Programming and Reasoning with Guarded Recursion for Coinductive Types. CoRR (2015)
Ales Bizjak, Lars Birkedal, Marino Miculan
A Model of Countable Nondeterminism in Guarded Type Theory. RTA-TLCA (2014)
Lars Birkedal, Ales Bizjak, Jan Schwinghammer
Step-Indexed Relational Reasoning for Countable Nondeterminism. Log. Methods Comput. Sci. 9 (4) (2013)