Decision Procedures for Algebraic Data Types with Abstractions

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.

Published in:
Acm Sigplan Notices, 45, 199-210
Presented at:
ACM Symp. Principles of Programming Languages (POPL), 2010

 Record created 2010-02-14, last modified 2018-03-17

Rate this document:

Rate this document:
(Not yet reviewed)