Modularity of strong normalization in the algebraic-λ-cube

DOI10.1017/S095679689700289XzbMath0918.03010OpenAlexW2082162654MaRDI QIDQ4234771

Maribel Fernández, Herman Geuvers, Franco Barbanera

Publication date: 16 March 1999

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s095679689700289x

zbMATH Keywords

strong normalizationlocal confluencealgebraic-\(\lambda\)-cubehigher-order algebraic rewriting

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

Nominal rewriting, (Head-)normalization of typeable rewrite systems, Problems in rewriting III, On the power of simple diagrams, Normalization results for typeable rewrite systems, Expressing combinatory reduction systems derivations in the rewriting calculus, On modular properties of higher order extensional lambda calculi, Size-based termination of higher-order rewriting, Abstract data type systems, A short and flexible proof of strong normalization for the calculus of constructions, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, The Computability Path Ordering: The End of a Quest, Intersection type assignment systems with higher-order algebraic rewriting, Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules, On the confluence of lambda-calculus with conditional rewriting, Semantic foundations for generalized rewrite theories, Unnamed Item, Inductive-data-type systems, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering