Toward a geometry for syntax

DOI10.1007/978-3-031-68934-5_15MaRDI QIDQ6911852zbMATH OpenFDO

Authors Jonathan Sterling

Publication date 24 October 2025

Full work available at URL https://doi.org/10.1007/978-3-031-68934-5_15

zbMATH Keywords

Artin gluingcategory theorydependent type theorynatural modelsnormalisationsynthetic Tait computabilitytopos theory

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) Category theory; homological algebra (18-XX)

Cites work

• A machine-checked proof of the odd order theorem
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
• A type theory for synthetic -categories
• Canonicity and normalization for dependent type theory
• Categorical reconstruction of a reduction free normalization proof
• Formal proof - the four color theorem
• Handbook of Spatial Logics
• Higher Topos Theory (AM-170)
• Homotopy theoretic models of identity types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3521951 (Why is no real title available?)
• scientific article; zbMATH DE number 3574077 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 1342278 (Why is no real title available?)
• scientific article; zbMATH DE number 512784 (Why is no real title available?)
• scientific article; zbMATH DE number 1078585 (Why is no real title available?)
• scientific article; zbMATH DE number 6816943 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• scientific article; zbMATH DE number 2247252 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Internal type theory
• Liquid tensor experiment
• Logical relations and the typed λ-calculus
• Mathematical logic as based on the theory of types.
• Modalities in homotopy type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Natural models of homotopy type theory
• Normalization for multimodal type theory
• Polynomial functors and polynomial monads
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Seminar of algebraic geometry du Bois-Marie 1963--1964. Topos theory and étale cohomology of schemes (SGA 4). Vol. 1: Topos theory. Exp. I--IV
• Sheaf semantics of termination-insensitive noninterference
• Singular coverings of toposes
• The Lean theorem prover (system description)
• The local universes model: an overlooked coherence construction for dependent type theories
• The principles of Mathematics. Vol I.
• Topo-logie
• Univalence for inverse diagrams and homotopy canonicity
• Über Grenzzahlen und Mengenbereiche. Neue Untersuchungen über die Grundlagen der Mengenlehre.

Cited in

(1)

• Controlling unfolding in type theory

This page was built for publication: Toward a geometry for syntax

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