Simulating expansions without expansions

DOI10.1017/S0960129500000505zbMath0831.03004MaRDI QIDQ4322432

Roberto Di Cosmo, Delia Kesner

Publication date: 18 February 1996

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

confluencerewriting systemstrong normalizationsumstyped \(\lambda\)-calculusbounded recursionexpansion rulesextensional equalitiesunbounded recursion

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

Some lambda calculi with categorical sums and products ⋮ On the power of simple diagrams ⋮ Combining algebraic rewriting, extensional lambda calculi, and fixpoints ⋮ Normal Higher-Order Termination ⋮ Developing developments ⋮ Extensional proofs in a propositional logic modulo isomorphisms ⋮ A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object ⋮ Combining first order algebraic rewriting systems, recursion and extensional lambda calculi ⋮ Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ A Local Graph-rewriting System for Deciding Equality in Sum-product Theories

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On the implementation of abstract data types by programming language constructs
• Strong normalization for typed terms with surjective pairing
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus