Decision Procedures for Algebraic Data Types with Abstractions

paper ps   
We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term algebra homomorphisms) mapping algebraic data type values into values in other decidable theories (e.g. sets, multisets, lists, integers, booleans). Each instance of our decision procedure family is sound; we identify a widely applicable many-to-one condition on abstraction functions that implies the completeness. Complete instances of our decision procedure include the following correctness statements: 1) a functional data structure implementation satisfies a recursively specified invariant, 2) such data structure conforms to a contract given in terms of sets, multisets, lists, sizes, or heights, 3) a transformation of a formula (or lambda term) abstract syntax tree changes the set of free variables in the specified way.

Citation

Philippe Suter, Mirco Dotta, and Viktor Kuncak. Decision procedures for algebraic data types with abstractions. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), 2010.

BibTex Entry

@inproceedings{SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions,
  author = {Philippe Suter and Mirco Dotta and Viktor Kuncak},
  title = {Decision Procedures for Algebraic Data Types with Abstractions},
  year = 2010,
  booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
  abstract = {We describe a family of decision procedures that extend the
decision procedure for quantifier-free constraints on
recursive algebraic data types (term algebras) to support
recursive abstraction functions. Our abstraction functions
are catamorphisms (term algebra homomorphisms) mapping
algebraic data type values into values in other decidable
theories (e.g. sets, multisets, lists, integers, booleans).
Each instance of our decision procedure family is sound;
we identify a widely applicable many-to-one condition on
abstraction functions that implies the completeness. Complete
instances of our decision procedure include the following
correctness statements: 1) a functional data
structure implementation satisfies a recursively specified
invariant, 2) such data structure conforms to a contract
given in terms of sets, multisets, lists, sizes, or heights, 3) a
transformation of a formula (or 
lambda term) abstract syntax tree changes the set of free variables in
the specified way.}
}