Showing 1–10 of 10 results for author: Angiuli, C

A dependently-typed calculus of event telicity and culminativity

Authors: Pavel Kovalev, Carlo Angiuli

Abstract: 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 sentences. Our framework consists of two parts. In the nominal domain, we model the boundedness of noun phrases and its relationship to subtyping, delimited quantities, and adjectival modification. In the verbal domain we… ▽ More 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 sentences. Our framework consists of two parts. In the nominal domain, we model the boundedness of noun phrases and its relationship to subtyping, delimited quantities, and adjectival modification. In the verbal domain we define a dependent event calculus, modeling telic events as those whose undergoer is bounded, culminating events as telic events that achieve their inherent endpoint, and consider adverbial modification. In both domains we pay particular attention to associated entailments. Our framework is defined as an extension of intensional Martin-Löf dependent type theory, and the rules and examples in this paper have been formalized in the Agda proof assistant. △ Less

Submitted 7 June, 2025; originally announced June 2025.

Comments: 52 pages, Agda formalization available at https://doi.org/10.5281/zenodo.15602617

Controlling unfolding in type theory

Authors: Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal

Abstract: We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In… ▽ More We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it. △ Less

Submitted 11 October, 2022; originally announced October 2022.

Normalization for Cubical Type Theory

Authors: Jonathan Sterling, Carlo Angiuli

Abstract: 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 result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of $β/η$-normal forms. As corollaries we obtain both decidability of judgmental equalit… ▽ More 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 result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of $β/η$-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors. △ Less

Submitted 19 April, 2021; v1 submitted 27 January, 2021; originally announced January 2021.

Comments: LICS 2021

Journal ref: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021, pp. 1-15

Internalizing Representation Independence with Univalence

Authors: Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner

Abstract: In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theo… ▽ More In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way. △ Less

Submitted 25 October, 2020; v1 submitted 11 September, 2020; originally announced September 2020.

Comments: 30 pages; ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2021

A Cubical Language for Bishop Sets

Authors: Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

Abstract: 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 proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT… ▽ More 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 proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing. △ Less

Submitted 28 March, 2022; v1 submitted 3 March, 2020; originally announced March 2020.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (March 29, 2022) lmcs:9069

Cubical Syntax for Reflection-Free Extensional Equality

Authors: Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

Abstract: We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity types principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in… ▽ More We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity types principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel cubical extension (independently proposed by Awodey) of the logical families or categorical gluing argument inspired by Coquand and Shulman: every closed element of boolean type is derivably equal to either 'true' or 'false'. △ Less

Submitted 6 June, 2019; v1 submitted 17 April, 2019; originally announced April 2019.

Comments: Extended version; International Conference on Formal Structures for Computation and Deduction (FSCD), 2019

The RedPRL Proof Assistant (Invited Paper)

Authors: Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou, Robert Harper, Jonathan Sterling

Abstract: RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory,… ▽ More RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths. △ Less

Submitted 5 July, 2018; originally announced July 2018.

Comments: In Proceedings LFMTP 2018, arXiv:1807.01352

Journal ref: EPTCS 274, 2018, pp. 1-10

Computational Higher Type Theory III: Univalent Universes and Exact Equality

Authors: Carlo Angiuli, Kuen-Bang Hou, Robert Harper

Abstract: This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype unive… ▽ More This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype universes. As in Parts I and II, the main result is a canonicity theorem stating that closed terms of boolean type evaluate to either true or false. This establishes the computational interpretation of Cartesian cubical higher type theory based on cubical programs equipped with a deterministic operational semantics. △ Less

Submitted 5 December, 2017; originally announced December 2017.

Comments: 71 pages

Computational Higher Type Theory II: Dependent Cubical Realizability

Authors: Carlo Angiuli, Robert Harper

Abstract: This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I, and extend it to a meaning explanation of dependent higher-dimensional type theory. This extension requires generalizing the computational Kan condition given in Pa… ▽ More This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I, and extend it to a meaning explanation of dependent higher-dimensional type theory. This extension requires generalizing the computational Kan condition given in Part I, and considering the action of type families on paths. We define identification types, which classify identifications (paths) in a type, and dependent function and pair types. The main result is a canonicity theorem, which states that a closed term of boolean type evaluates to either true or false. This result establishes the first computational interpretation of higher dependent type theory by giving a deterministic operational semantics for its programs, including operations that realize the Kan condition. △ Less

Submitted 26 April, 2017; v1 submitted 30 June, 2016; originally announced June 2016.

Comments: 65 pages. v2: added sections A.1, A.2. v3: added sections A.3, A.4. arXiv admin note: text overlap with arXiv:1604.08873

Computational Higher Type Theory I: Abstract Cubical Realizability

Authors: Carlo Angiuli, Robert Harper, Todd Wilson

Abstract: Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for constructive type theory define the concept of a type in terms of computation. Briefly, a type is a complete (closed) program that evaluates to a canonical type whose members are complete programs that evaluate to canoni… ▽ More Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for constructive type theory define the concept of a type in terms of computation. Briefly, a type is a complete (closed) program that evaluates to a canonical type whose members are complete programs that evaluate to canonical elements of that type. The explanation is extended to incomplete (open) programs by functionality: types and elements must respect equality in their free variables. Equality is evidence-free---two types or elements are at most equal---and equal things are implicitly interchangeable in all contexts. Higher-dimensional type theory extends type theory to account for identifications of types and elements. An identification witnesses that two types or elements are explicitly interchangeable in all contexts by an explicit transport, or coercion, operation. There must be sufficiently many identifications, which is ensured by imposing a generalized form of the Kan condition from homotopy theory. Here we provide a Martin-Löf-style meaning explanation of simple higher-dimensional type theory based on a programming language that includes Kan-like constructs witnessing the computational meaning of the higher structure of types. The treatment includes an example of a higher inductive type (namely, the 1-dimensional sphere) and an example of Voevodsky's univalence principle, which identifies equivalent types. The main result is a computational canonicity theorem that validates the computational interpretation: a closed boolean expression must always evaluate to a boolean value, even in the presence of higher-dimensional structure. This provides the first fully computational formulation of higher-dimensional type theory. △ Less

Submitted 14 June, 2016; v1 submitted 29 April, 2016; originally announced April 2016.

Comments: 39 pages. v2: added abstract, minor corrections