Functional completeness of cartesian categories

DOI10.1016/0003-4843(74)90003-5MaRDI QIDQ4767105zbMATH OpenOpenAlexWikidataFDO

Authors J. Lambek

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

Mathematics Subject Classification ID

Classical first-order logic (03B10) Intermediate logics (03B55) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Foundations, relations to logic and deductive systems (18A15)

Cited in

(25)

• Ologisms
• Composition of deductions within the propositions-as-types paradigm
• Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
• scientific article; zbMATH DE number 4144224 (Why is no real title available?)
• Algebra of constructions. I. The word problem for partial algebras
• Models of deduction
• scientific article; zbMATH DE number 7779295 (Why is no real title available?)
• From types to sets
• Intuitionist type theory and foundations
• Inferential Semantics
• Identity of Proofs Based on Normalization and Generality
• Deductive Completeness
• Pre-recursive categories
• scientific article; zbMATH DE number 3512376 (Why is no real title available?)
• Least fixpoints of endofunctors of cartesian closed categories
• On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
• Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic
• The Deduction Theorem (Before and After Herbrand)
• Intuitionist type theory and the free topos
• scientific article; zbMATH DE number 3741397 (Why is no real title available?)
• Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions
• Closure functions and general iterates as reflectors
• Decomposing typed lambda calculus into a couple of categorical programming languages
• Polycategories
• Aspects of categorical recursion theory

This page was built for publication: Functional completeness of cartesian categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4767105)