list | abstracts | bib ]

On Decision Procedures for Algebraic Data Types with Abstractions

paper pdf    paper ps   


We describe a parameterized decision procedure that extends the decision procedure for functional recursive algebraic data types (trees) with the ability to specify and reason about abstractions of data structures. The abstract values are specified using recursive abstraction functions that map trees into other data types that have decidable theories. Our result yields a decidable logic which can be used to prove that implementations of functional data structures satisfy recursively specified invariants and conform to interfaces given in terms of sets, multisets, or lists, or to increase the automation in proof assistants.


Philippe Suter, Mirco Dotta, and Viktor Kuncak. On decision procedures for algebraic data types with abstractions. Technical Report LARA-REPORT-2009-003, EPFL, 16 July 2009.

BibTex Entry

  author = {Philippe Suter and Mirco Dotta and Viktor Kuncak},
  title = {On Decision Procedures for Algebraic Data Types with Abstractions},
  institution = {EPFL},
  year = 2009,
  number = {LARA-REPORT-2009-003},
  month = {16 July},
  localurl = {}

list | abstracts | bib ]