Ales Bizjak

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