Synthesis of programs in abstract data types

In this paper we propose a method for program synthesis from constructive proofs based on a particular proof strategy, we call dischargeable set construction. This proof-strategy allows to build proofs in which active patterns (sequences of application of rules with proper computational content) can be distinguished from correctness patterns (concerning correctness properties of the algorithm implicitly contained in the proof). The synthesis method associates with every active pattern of the proof a program schema (in an imperative language) translating only the computational content of the proof. One of the main features of our method is that it can be applied to a variety of theories formalizing ADT's and classes of ADT's. Here we will discuss the method and the computational content of some principles of particular interest in the context of some classes of ADT's.