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 (11)

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

• 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
• Unnamed Item

This page was built for publication: Simulating expansions without expansions