Modularity of termination and confluence in combinations of rewrite systems with λω

DOI10.1007/3-540-56939-1_110zbMath1418.68110OpenAlexW107542622MaRDI QIDQ4630300

Maribel Fernández, Franco Barbanera

Publication date: 29 March 2019

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-56939-1_110

zbMATH Keywords

higher-order functioncritical pairrecursive definitionmodular propertyfunction symbol

Mathematics Subject Classification ID

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

Related Items

Variants of the basic calculus of constructions, More problems in rewriting, Problems in rewriting III, On modular properties of higher order extensional lambda calculi, Abstract data type systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Counterexamples to termination for the direct sum of term rewriting systems
• The calculus of constructions
• On termination of the direct sum of term-rewriting systems
• Polymorphic rewriting conserves algebraic strong normalization
• Complete restrictions of the intersection type discipline
• Polymorphic rewriting conserves algebraic confluence
• On theories with a combinatorial definition of 'equivalence'
• A filter lambda model and the completeness of type assignment
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Introduction to generalized type systems
• On the Church-Rosser property for the direct sum of term rewriting systems
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• Higher-order unification, polymorphism, and subsorts