Follow
Ale¹ Bizjak
Ale¹ Bizjak
Formerly postdoctoral researcher, Aarhus University, currently software architect at Concordium
Verified email at alesb.com - Homepage
Title
Cited by
Cited by
Year
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
R Jung, R Krebbers, JH Jourdan, A Bizjak, L Birkedal, D Dreyer
Journal of Functional Programming 1, 2018
5062018
The essence of higher-order concurrent separation logic
R Krebbers, R Jung, A Bizjak, JH Jourdan, D Dreyer, L Birkedal
Programming Languages and Systems: 26th European Symposium on Programming …, 2017
1762017
Guarded Dependent Type Theory with Coinductive Types
A Bizjak, R Clouston, HB Grathwohl, L Birkedal
86*
Guarded cubical type theory: Path equality for guarded recursion
L Birkedal, A Bizjak, R Clouston, HB Grathwohl, B Spitters, A Vezzosi
arXiv preprint arXiv:1606.05223, 2016
73*2016
Step-Indexed Logical Relations for Probability
A Bizjak, L Birkedal
Foundations of Software Science and Computation Structures 9034, 279-294, 2015
642015
Programming and reasoning with guarded recursion for coinductive types
R Clouston, A Bizjak, HB Grathwohl, L Birkedal
Foundations of Software Science and Computation Structures 9034, 407-421, 2015
442015
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
R Clouston, A Bizjak, HB Grathwohl, L Birkedal
Logical Methods in Computer Science, 2016
362016
Iron: Managing obligations in higher-order concurrent separation logic
A Bizjak, D Gratzer, R Krebbers, L Birkedal
https://iris-project.org/pdfs/2019-popl-iron-final.pdf, 2018
352018
A model of countable nondeterminism in guarded type theory
A Bizjak, L Birkedal, M Miculan
Rewriting and Typed Lambda Calculi 8560, 108-123, 2014
312014
On models of higher-order separation logic
A Bizjak, L Birkedal
Electronic Notes in Theoretical Computer Science 336, 57-78, 2018
252018
A model of guarded recursion with clock synchronisation
A Bizjak, RE Møgelberg
Mathematical Foundations of Programming Semantics, 2015
252015
Denotational semantics for guarded dependent type theory
A Bizjak, RE Møgelberg
Mathematical Structures in Computer Science 30 (4), 342-378, 2020
242020
Step-indexed relational reasoning for countable nondeterminism
L Birkedal, A Bizjak, J Schwinghammer
Logical Methods in Computer Science 9 (4), 2013
21*2013
Relational reasoning for markov chains in a probabilistic guarded lambda calculus
A Aguirre, G Barthe, L Birkedal, A Bizjak, M Gaboardi, D Garg
Programming Languages and Systems: 27th European Symposium on Programming …, 2018
202018
ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages
F Sieczkowski, A Bizjak, L Birkedal
Interactive Theorem Proving, 2015
172015
Lecture notes on iris: Higher-order concurrent separation logic
L Birkedal, A Bizjak
Lectures notes, September, 2020
162020
A Taste of Categorical Logic—tutorial notes
L Birkedal, A Bizjak
102014
On semantics and applications of guarded recursion
A Bizjak
Department of Computer Science, Aarhus University, 2016
82016
Alg user manual
A Bizjak, A Bauer
Faculty of Mathematics and Physics, University of Ljubljana, 2011
52011
Some theorems about mutually recursive domain equations in the category of preordered COFEs
A Bizjak
Unpublished note. Available at http://cs. au. dk/~ abizjak/documents/notes …, 2017
42017
The system can't perform the operation now. Try again later.
Articles 1–20