Modularity of strong normalization in the algebraic-λ-cube
From MaRDI portal
Recommendations
- Modular properties of algebraic type systems
- On modular properties of higher order extensional lambda calculi
- Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
- scientific article; zbMATH DE number 4124996
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
Cited in
(22)- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Normalization results for typeable rewrite systems
- Abstract data type systems
- Nominal rewriting
- Semantic foundations for generalized rewrite theories
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- The Computability Path Ordering: The End of a Quest
- On modular properties of higher order extensional lambda calculi
- Size-based termination of higher-order rewriting
- Modular properties of algebraic type systems
- (Head-)normalization of typeable rewrite systems
- Problems in rewriting III
- On the power of simple diagrams
- scientific article; zbMATH DE number 7566074 (Why is no real title available?)
- Inductive-data-type systems
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- A short and flexible proof of strong normalization for the calculus of constructions
- Intersection type assignment systems with higher-order algebraic rewriting
- Type safety of rewrite rules in dependent types
- Expressing combinatory reduction systems derivations in the rewriting calculus
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- On the confluence of lambda-calculus with conditional rewriting
This page was built for publication: Modularity of strong normalization in the algebraic-λ-cube
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4234771)
