Abstract data type systems
From MaRDI portal
Publication:1391729
DOI10.1016/S0304-3975(96)00161-2zbMath0901.68121MaRDI QIDQ1391729
Jean-Pierre Jouannaud, Mitsuhiro Okada
Publication date: 22 July 1998
Published in: Theoretical Computer Science (Search for Journal in Brave)
68Q65: Abstract data types; algebraic specification
Related Items
Inductive-data-type systems, Expressing combinatory reduction systems derivations in the rewriting calculus, Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering, Pattern matching as cut elimination, Specification and proof in membership equational logic, Semantic foundations for generalized rewrite theories, The Computability Path Ordering: The End of a Quest
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
