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.}
}