28 citations · 112 across the 10 of their papers we have counts for
12 papers
Revisiting Soundness for Occurrence Typing, Semantically
Yuquan Fu, Carlo Angiuli, Sam Tobin-Hochstadt
Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms c…
A dependently-typed calculus of event telicity and culminativity
Pavel Kovalev, Carlo Angiuli
We present a dependently-typed cross-linguistic framework for analyzing the telicity and culminativity of events, accompanied by examples of using our framework to model English se…
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…
Normalization for Cubical Type Theory
Jonathan Sterling, Carlo Angiuli
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization res…
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg +1
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are rela…
A Cubical Language for Bishop Sets
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity…