28 citations · 54 across the 4 of their papers we have counts for
8 papers
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Alejandro Aguirre, Gilles Barthe, Lars Birkedal +3
We extend the simply-typed guarded -calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic com…
Denotational semantics for guarded dependent type theory
Aleš Bizjak, Rasmus Ejlers Møgelberg
We present a new model of Guarded Dependent Type Theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with, and reason about coinductive…
Guarded Cubical Type Theory
Lars Birkedal, Aleš Bizjak, Ranald Clouston +3
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guard…
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
Lars Birkedal, Aleš Bizjak, Ranald Clouston +3
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guard…
Guarded Dependent Type Theory with Coinductive Types
Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston +2
We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later' modality and clock quantifiers for programming and proving with guarded recursiv…
Programming and Reasoning with Guarded Recursion for Coinductive Types
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl +1
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures th…
Step-Indexed Logical Relations for Probability (long version)
Aleš Bizjak, Lars Birkedal
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabil…
Step-Indexed Relational Reasoning for Countable Nondeterminism
Lars Birkedal, Aleš Bizjak, Jan Schwinghammer
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Be…