Polymorphic rewriting conserves algebraic strong normalization

DOI10.1016/0304-3975(91)90037-3zbMath0745.68065OpenAlexW1999683854MaRDI QIDQ1176244

Val Breazu-Tannen, Jean H. Gallier

Publication date: 25 June 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cis_reports/546

zbMATH Keywords

many-sorted algebraic term rewriting systemspolymorphic lambda term rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Termination of combined (rewrite and λ-calculus) systems, Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved, Higher-order unification via combinators, Nominal rewriting, Harnessing First Order Termination Provers Using Higher Order Dependency Pairs, Adding algebraic rewriting to the untyped lambda calculus (extended abstract), On the power of simple diagrams, Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Normal forms in combinatory logic, On modular properties of higher order extensional lambda calculi, Abstract data type systems, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Modularity of termination and confluence in combinations of rewrite systems with λω, Intersection type assignment systems with higher-order algebraic rewriting, A combinatory logic approach to higher-order E-unification, Modular properties of algebraic type systems, A typed, algebraic, computational lambda-calculus, Unnamed Item, Inductive-data-type systems, Lambda calculus with algebraic simplification for reduction parallelisation: Extended study, Modularity of confluence: A simplified proof

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• The calculus of constructions
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Complete sets of transformations for general E-unification
• Higher-order unification revisited: Complete sets of transformations
• Logical relations and the typed λ-calculus
• Completeness, invariance and λ-definability
• On the Church-Rosser property for the direct sum of term rewriting systems
• Intensional interpretations of functionals of finite type I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item