9 citations · 23 across the 4 of their papers we have counts for
6 papers · 1 filter
Two Guarded Recursive Powerdomains for Applicative Simulation
Rasmus Ejlers Møgelberg, Andrea Vezzosi
Clocked Cubical Type Theory is a new type theory combining the power of guarded recursion with univalence and higher inductive types (HITs). This type theory can be used as a metal…
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi
Guarded recursion is a powerful modal approach to recursion that can be seen as an abstract form of step-indexing. It is currently used extensively in separation logic to model pro…
Partial Univalence in n-truncated Type Theory
Christian Sattler, Andrea Vezzosi
It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial auto…
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…
Functions out of Higher Truncations
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence…