scientific article; zbMATH DE number 226803
From MaRDI portal
Publication:5286647
zbMath0790.68068MaRDI QIDQ5286647
Publication date: 5 July 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Semantics in the theory of computing (68Q55) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theories (e.g., algebraic theories), structure, and semantics (18C10) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Metamathematics of constructive systems (03F50)
Related Items (53)
Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory ⋮ The intrinsic topology of Martin-Löf universes ⋮ On completeness and cocompleteness in and around small categories ⋮ Doctrines, modalities and comonads ⋮ Unnamed Item ⋮ Martin Hofmann’s contributions to type theory: Groupoids and univalence ⋮ On generalized algebraic theories and categories with families ⋮ Coreflections in algebraic quantum logic ⋮ Observability in the univalent universe ⋮ Finitary type theories with and without contexts ⋮ The metatheory of UTT ⋮ Models of HoTT and the Constructive View of Theories ⋮ Proving strong normalization of CC by modifying realizability semantics ⋮ Elimination of extensionality in Martin-Löf type theory ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Typed operational semantics for higher-order subtyping. ⋮ Martin-Löf identity types in C-systems ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Unnamed Item ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ An intuitionistic set-theoretical model of fully dependent CC ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ Semantical analysis of contextual types ⋮ Classical predicative logic-enriched type theories ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ The algebra of partial equivalence relations ⋮ Collapsing partial combinatory algebras ⋮ A simple model construction for the Calculus of Constructions ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Independence of the induction principle and the axiom of choice in the pure calculus of constructions ⋮ A dependent type theory with abstractable names ⋮ The proof monad ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Realizability models refuting Ishihara's boundedness principle ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The homotopy theory of type theories ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Semantics of higher inductive types ⋮ Type Theory Should Eat Itself ⋮ Dependent Types and Fibred Computational Effects ⋮ Kripke Semantics for Martin-Löf’s Extensional Type Theory ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Joyal's arithmetic universes via type theory ⋮ Pure Type System conversion is always typable ⋮ Containers: Constructing strictly positive types ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ C-systems defined by universe categories: presheaves ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories ⋮ Type Theory and Homotopy ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed ⋮ Extensional equality preservation and verified generic programming
This page was built for publication:
