Abstract data type systems
From MaRDI portal
Publication:1391729
DOI10.1016/S0304-3975(96)00161-2zbMath0901.68121MaRDI QIDQ1391729
Mitsuhiro Okada, Jean-Pierre Jouannaud
Publication date: 22 July 1998
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items (10)
Pattern matching as cut elimination ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Expressing combinatory reduction systems derivations in the rewriting calculus ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ The Computability Path Ordering: The End of a Quest ⋮ Specification and proof in membership equational logic ⋮ Unnamed Item ⋮ Semantic foundations for generalized rewrite theories ⋮ Inductive-data-type systems ⋮ Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unification in Boolean rings and Abelian groups
- Orderings for term-rewriting systems
- Proofs by induction in equational theories with constructors
- A rationale for conditional equational programming
- Polymorphic rewriting conserves algebraic strong normalization
- Modularity of simple termination of term rewriting systems with shared constructors
- Adding algebraic rewriting to the untyped lambda calculus
- A theory of type polymorphism in programming
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
- Automatic proofs by induction in theories without constructors
- Positive and negative results for higher-order disunification
- Semantic confluence tests and completion methods
- Completion of a Set of Rules Modulo a Set of Equations
- Programming with equalities, subsorts, overloading, and parametrization in OBJ
- Modularity of strong normalization in the algebraic-λ-cube
- Modularity of termination and confluence in combinations of rewrite systems with λω
- Pumping, cleaning and symbolic constraints solving
- A termination ordering for higher order rewrite systems
- On the Church-Rosser property for the direct sum of term rewriting systems
This page was built for publication: Abstract data type systems
