scientific article; zbMATH DE number 1241699

zbMath0919.68083MaRDI QIDQ4225149

Martin Hofmann

Publication date: 18 January 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

category-theoretic semanticscategories with families

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items (55)

Categorical structures for type theory in univalent foundations ⋮ A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory ⋮ Games for Dependent Types ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Constructive sheaf models of type theory ⋮ On generalized algebraic theories and categories with families ⋮ Martin-Löf complexes ⋮ Combinatorial realizability models of type theory ⋮ Dependently Sorted Logic ⋮ Unnamed Item ⋮ The Local Universes Model ⋮ Reduction Free Normalisation for a proof irrelevant type of propositions ⋮ Two-level type theory and applications ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ Semantical analysis of contextual types ⋮ Induction-recursion and initial algebras. ⋮ Inductively generated formal topologies. ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A presheaf model of parametric type theory ⋮ Unnamed Item ⋮ Denotational semantics for guarded dependent type theory ⋮ Graded modal dependent type theory ⋮ Univalent polymorphism ⋮ Internal type theory ⋮ Conservativity of equality reflection over intensional type theory ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ The identity type weak factorisation system ⋮ The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective ⋮ Revisiting the categorical interpretation of dependent type theory ⋮ A dependent type theory with abstractable names ⋮ Syntactic approaches to opetopes ⋮ 2-Dimensional Directed Type Theory ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Type Theory Should Eat Itself ⋮ Dependent Types and Fibred Computational Effects ⋮ Modal dependent type theory and dependent right adjoints ⋮ Kripke Semantics for Martin-Löf’s Extensional Type Theory ⋮ On the strength of dependent products in the type theory of Martin-Löf ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The universal exponentiable arrow ⋮ Categories with families and first-order logic with dependent sorts ⋮ Safe recursion with higher types and BCK-algebra ⋮ Models of Type Theory Based on Moore Paths ⋮ Containers: Constructing strictly positive types ⋮ Unnamed Item ⋮ Type Theory and Homotopy ⋮ Natural models of homotopy type theory ⋮ Model structure on the universe of all types in interval type theory

This page was built for publication: