Abstract
We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language λProlog. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. We argue that this approach is especially effective in realizing transformations that analyze binding structure. We do this by describing concise encodings in λProlog for transformations like typed closure conversion and code hoisting that are sensitive to such structure and by showing how to prove their correctness using Abella.
| Original language | English (US) |
|---|---|
| Title of host publication | Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings |
| Editors | Peter Thiemann |
| Publisher | Springer Verlag |
| Pages | 752-779 |
| Number of pages | 28 |
| ISBN (Print) | 9783662494974 |
| DOIs | |
| State | Published - 2016 |
| Event | 25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands Duration: Apr 2 2016 → Apr 8 2016 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 9632 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 |
|---|---|
| Country/Territory | Netherlands |
| City | Eindhoven |
| Period | 4/2/16 → 4/8/16 |
Bibliographical note
Funding Information:We are grateful to David Baelde for his help in phrasing the definition of the logical relation in Sect. . The paper has benefited from many suggestions from its reviewers. This work has been supported by the National Science Foundation grant CCF-0917140 and by the University of Minnesota through a Doctoral Dissertation Fellowship and a Grant-in-Aid of Research. Opinions, findings and conclusions or recommendations that are manifest in this material are those of the participants and do not necessarily reflect the views of the NSF.
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2016.