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

Yuting Wang; Gopalan Nadathur

doi:10.1007/978-3-662-49498-1_29

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

Yuting Wang, Gopalan Nadathur

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 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 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	https://doi.org/10.1007/978-3-662-49498-1_29
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

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2016.

Publisher link

10.1007/978-3-662-49498-1_29

Find It

Find It at U of M Libraries

Cite this

Wang, Y., & Nadathur, G. (2016). A higher-order abstract syntax approach to verified transformations on functional programs. In P. Thiemann (Ed.), 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 (pp. 752-779). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9632). Springer Verlag. https://doi.org/10.1007/978-3-662-49498-1_29

A higher-order abstract syntax approach to verified transformations on functional programs. / Wang, Yuting; Nadathur, Gopalan.
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. ed. / Peter Thiemann. Springer Verlag, 2016. p. 752-779 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9632).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Wang, Y & Nadathur, G 2016, A higher-order abstract syntax approach to verified transformations on functional programs. in P Thiemann (ed.), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9632, Springer Verlag, pp. 752-779, 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, 4/2/16. https://doi.org/10.1007/978-3-662-49498-1_29

Wang Y, Nadathur G. A higher-order abstract syntax approach to verified transformations on functional programs. In Thiemann P, editor, 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. Springer Verlag. 2016. p. 752-779. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-49498-1_29

Wang, Yuting ; Nadathur, Gopalan. / A higher-order abstract syntax approach to verified transformations on functional programs. 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. editor / Peter Thiemann. Springer Verlag, 2016. pp. 752-779 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d9b0e0edc9914c2a9d4a1d5b86201eaf,

title = "A higher-order abstract syntax approach to verified transformations on functional programs",

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.",

author = "Yuting Wang and Gopalan Nadathur",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2016.; 25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",

year = "2016",

doi = "10.1007/978-3-662-49498-1_29",

language = "English (US)",

isbn = "9783662494974",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "752--779",

editor = "Peter Thiemann",

booktitle = "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",

}

TY - GEN

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

AU - Wang, Yuting

AU - Nadathur, Gopalan

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84961691703&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84961691703&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-49498-1_29

DO - 10.1007/978-3-662-49498-1_29

M3 - Conference contribution

AN - SCOPUS:84961691703

SN - 9783662494974

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 752

EP - 779

BT - 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

A2 - Thiemann, Peter

PB - Springer Verlag

T2 - 25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016

Y2 - 2 April 2016 through 8 April 2016

ER -

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

Abstract

Publication series

Other

Bibliographical note

Publisher link

Find It

Other files and links

Fingerprint

Cite this