Controlling unfolding in type theory

DOI10.1017/S0960129525100327MaRDI QIDQ6879482zbMATH OpenFDO

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

Publication date 30 December 2025

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/S0960129525100327

zbMATH Keywords

proof assistantsdependent type theorycategorical type theory

Mathematics Subject Classification ID

Type theory (03B38)

Cites work

• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3574077 (Why is no real title available?)
• scientific article; zbMATH DE number 512784 (Why is no real title available?)
• scientific article; zbMATH DE number 2079014 (Why is no real title available?)
• A 2-categories companion
• A general framework for the semantics of type theory
• A type system for higher-order modules
• A type theory for synthetic -categories
• An algorithm for type-checking dependent types
• Aspects of topoi
• Canonicity for cubical type theory
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Extensional equivalence and singleton types
• Featherweight VeriFast
• Homotopy type theory. Univalent foundations of mathematics
• Internal type theory
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Natural models of homotopy type theory
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Syntax and models of Cartesian cubical type theory
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• Topo-logie
• Toward a geometry for syntax

This page was built for publication: Controlling unfolding in type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6879482)