Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x] ofT

DOI10.1051/ITA:1999115MaRDI QIDQ4718892zbMATHOpenAlexFDO

Authors Anne Preller, P. Duroux

Publication date 17 May 2000

Published in RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL https://eudml.org/doc/221951

zbMATH Keywords

functional completenessdecidabilityCartesian closed categoriessimply typed lambda calculusrewrite systemgraph of generatorsinductive definition of normal terms

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Foundations, relations to logic and deductive systems (18A15)

Recommendations

• scientific article; zbMATH DE number 176742
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• Coherence in Cartesian closed categories and the generality of proofs
• scientific article; zbMATH DE number 4103048

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 733666 (Why is no real title available?)
• Algebra of constructions. I. The word problem for partial algebras
• Normalization and the Yoneda embedding

This page was built for publication: Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x] ofT

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