scientific article
From MaRDI portal
Publication:4036571
zbMath0769.68056MaRDI QIDQ4036571
Roberto Di Cosmo, Pierre-Louis Curien
Publication date: 18 May 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
decidabilityterminal objectpolymorphic typesconfluent rewriting system\(\lambda\)-calculus extended with surjective pairingfull equational theory underlying cartesian closed categoriespolymorphic extensions
Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)
Related Items
Some lambda calculi with categorical sums and products, Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract), Categorical abstract machines for higher-order typed \(\lambda\)-calculi, Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Embedding of a free cartesian-closed category into the category of sets, Subtyping + extensionality: Confluence of βηtop reduction in F≤, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, Structures definable in polymorphism, Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
