A higher-order abstract syntax approach to verified transformations on functional programs

Yuting Wang, Gopalan Nadathur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

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 languageEnglish (US)
Title of host publicationProgramming 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
EditorsPeter Thiemann
PublisherSpringer Verlag
Pages752-779
Number of pages28
ISBN (Print)9783662494974
DOIs
StatePublished - 2016
Event25th 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 2016Apr 8 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9632
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
CountryNetherlands
CityEindhoven
Period4/2/164/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. 4.2. 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.

Fingerprint Dive into the research topics of 'A higher-order abstract syntax approach to verified transformations on functional programs'. Together they form a unique fingerprint.

Cite this