Polymorphic rewriting conserves algebraic strong normalization
From MaRDI portal
Publication:1176244
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
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
