Programming type-safe transformations using higher-order abstract syntax

• Main Authors: Olivier Savary Belanger, Stefan Monnier, Brigitte Pientka
• Format: Article in Journal/Newspaper
• Language: English
• Published: University of Bologna 2015
• Subjects: Logical frameworks; Certified Programming; Type-preserving Compilation; Electronic computers. Computer science; QA75.5-76.95; Analytic mechanics; QA801-939; Lambda; Beluga*
• Online Access: https://doi.org/10.6092/issn.1972-5787/5122; https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71

When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effort.In this paper, we show how Beluga's depend...