Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/3-540-48958-4_5 | LOPSTR |
Keywords | Field | DocType |
synthesis method associate,abstract data types,particular proof strategy,constructive proof,proper computational content,program schema,correctness property,computational content,particular interest,active pattern,correctness pattern,abstract data type | Abstract data type,Constructive proof,Program transformation,Program synthesis,Computer science,Correctness,Algorithm,Imperative programming,Theoretical computer science,Mathematical proof,Proof complexity | Conference |
Volume | ISSN | ISBN |
1559 | 0302-9743 | 3-540-65765-7 |
Citations | PageRank | References |
3 | 0.49 | 11 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alessandro Avellone | 1 | 63 | 7.66 |
| Mauro Ferrari | 2 | 61 | 5.67 |
| Pierangelo Miglioli | 3 | 227 | 26.86 |