Abstract data type systems

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)

zbMATH Keywords

abstract data type systems

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

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

• OBJ3
• Automath

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item