Cover Image

Controlling unfolding in type theory

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Gratzer, Daniel, Sterling, Jonathan, Angiuli, Carlo, Coquand, Thierry, Birkedal, Lars
Format:	Preprint
Published:	2022
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Unifying cubical and multimodal type theory
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2022)

Normalization for multimodal type theory
by: Gratzer, Daniel
Published: (2023)

Strict universes for Grothendieck topoi
by: Gratzer, Daniel, et al.
Published: (2022)

Reduction Free Normalisation for a proof irrelevant type of propositions
by: Coquand, Thierry
Published: (2021)

A denotationally-based program logic for higher-order store
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2023)

The $\infty$-category of $\infty$-categories in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2026)

A dependently-typed calculus of event telicity and culminativity
by: Kovalev, Pavel, et al.
Published: (2025)

Constructive higher sheaf models with applications to synthetic mathematics
by: Coquand, Thierry, et al.
Published: (2026)

Two Remarks about Game Semantics of Classical Logic
by: Coquand, Thierry
Published: (2026)

Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
by: Coquand, Thierry
Published: (2026)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
by: Gratzer, Daniel, et al.
Published: (2024)

Tensorial structure of the lifting doctrine in constructive domain theory
by: Sterling, Jonathan
Published: (2023)

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
by: Bezem, Marc, et al.
Published: (2026)

Reflexive graph lenses in univalent foundations
by: Sterling, Jonathan
Published: (2024)

The equivariant model structure on cartesian cubical sets
by: Awodey, Steve, et al.
Published: (2024)

Internalizing Representation Independence with Univalence
by: Angiuli, Carlo, et al.
Published: (2020)

Constructive theory of ordinals
by: Coquand, Thierry, et al.
Published: (2022)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

The Regular Element Property in Constructive Mathematics
by: Coquand, Thierry
Published: (2024)

Domains and Classifying Topoi
by: Sterling, Jonathan, et al.
Published: (2025)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
by: de Medeiros, Markus, et al.
Published: (2026)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

The Yoneda embedding in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2025)

Hofmann-Streicher lifting of fibred categories
by: Slattery, Andrew, et al.
Published: (2025)

Type Theory with Explicit Universe Polymorphism (revised and extended version)
by: Bezem, Marc, et al.
Published: (2022)

Directed univalence in simplicial homotopy type theory
by: Gratzer, Daniel, et al.
Published: (2024)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
by: de Jong, Tom, et al.
Published: (2026)

Almost-Sure Termination by Guarded Refinement
by: Gregersen, Simon Oddershede, et al.
Published: (2024)

Generic bidirectional typing for dependent type theories
by: Felicissimo, Thiago
Published: (2023)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

When is the partial map classifier a Sierpiński cone?
by: Pugh, Leoni, et al.
Published: (2025)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

Homotopy type theory as a language for diagrams of $\infty$-logoses
by: Uemura, Taichi
Published: (2022)

Formalizing two-level type theory with cofibrant exo-nat
by: Uskuplu, Elif
Published: (2023)

Directed type theory, with a twist
by: Rivera, Fernando Rafael Chu, et al.
Published: (2026)

Yet another cubical type theory, but via a semantic approach
by: Kapulkin, Chris, et al.
Published: (2025)

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
by: Spadetto, Matteo
Published: (2023)

Eliminating reversals from cubical type theories
by: Cavallo, Evan, et al.
Published: (2026)