scientific article
From MaRDI portal
Publication:3142163
zbMath0806.03043MaRDI QIDQ3142163
Publication date: 5 December 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
coherencecategorical logicinterpretation of first-order \(\lambda\)-calculus with dependent types in locally cartesian closed categories
Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)
Related Items (12)
A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories ⋮ Internal type theory ⋮ Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category ⋮ The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective ⋮ Revisiting the categorical interpretation of dependent type theory ⋮ Combinatorial structure of type dependency ⋮ Wellfounded trees in categories ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed
This page was built for publication:
