Functional completeness of cartesian categories
From MaRDI portal
Publication:4767105
DOI10.1016/0003-4843(74)90003-5zbMath0282.18004OpenAlexW2055942509WikidataQ60019634 ScholiaQ60019634MaRDI QIDQ4767105
Publication date: 1974
Published in: Annals of Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0003-4843(74)90003-5
Classical first-order logic (03B10) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Intermediate logics (03B55) Foundations, relations to logic and deductive systems (18A15)
Related Items (25)
Unnamed Item ⋮ Decomposing typed lambda calculus into a couple of categorical programming languages ⋮ Least fixpoints of endofunctors of cartesian closed categories ⋮ Algebra of constructions. I. The word problem for partial algebras ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions ⋮ From types to sets ⋮ The Deduction Theorem (Before and After Herbrand) ⋮ Intuitionist type theory and the free topos ⋮ Intuitionist type theory and foundations ⋮ Unnamed Item ⋮ Pre-recursive categories ⋮ Deductive Completeness ⋮ Unnamed Item ⋮ Composition of deductions within the propositions-as-types paradigm ⋮ Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic ⋮ Identity of Proofs Based on Normalization and Generality ⋮ Polycategories ⋮ Models of deduction ⋮ Unnamed Item ⋮ Inferential Semantics ⋮ Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types ⋮ Unnamed Item ⋮ Aspects of Categorical Recursion Theory ⋮ Closure functions and general iterates as reflectors
This page was built for publication: Functional completeness of cartesian categories
