Reasoning About Recursively Defined Data Structures
From MaRDI portal
Publication:3935457
DOI10.1145/322203.322204zbMath0477.68025OpenAlexW2095182415MaRDI QIDQ3935457
Publication date: 1980
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322203.322204
theorem provingdecidabilitysimplificationprogram verificationlogical complexityrecursive data structures
Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)
Related Items (23)
An algebraic semantics approach to the effective resolution of type equations ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ Fast algorithms for testing unsatisfiability of ground Horn clauses with equations ⋮ On the relationship of congruence closure and unification ⋮ Complexity, convexity and combinations of theories ⋮ Reasoning about algebraic data types with abstractions ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Decision procedures for term algebras with integer constraints ⋮ Unnamed Item ⋮ Inferring the equivalence of functional programs that mutate data ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Quantifier Elimination and Provers Integration ⋮ Automatic decidability and combinability ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Equivalence in functional languages with effects ⋮ Locality Results for Certain Extensions of Theories with Bridging Functions ⋮ Politeness and combination methods for theories with bridging functions ⋮ Colors Make Theories Hard ⋮ Quantifier elimination for infinite terms ⋮ Unification modulo lists with reverse relation with certain word equations ⋮ A view of computability on term algebras ⋮ An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types ⋮ Rewrite-Based Satisfiability Procedures for Recursive Data Structures
This page was built for publication: Reasoning About Recursively Defined Data Structures
