scientific article; zbMATH DE number 226803
From MaRDI portal
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
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
