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

DOI10.1051/ITA:1999115zbMATH Open0936.03011OpenAlexW2040138329MaRDI QIDQ4718892FDOQ4718892

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

Recommendations

• scientific article
• 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

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)

Cites Work

• Title not available (Why is that?)
• Normalization and the Yoneda embedding
• Title not available (Why is that?)
• Algebra of constructions. I. The word problem for partial algebras

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)