Programming type-safe transformations using higher-order abstract syntax

• Main Authors: Savary Belanger, Olivier, Monnier, Stefan, Pientka, Brigitte
• Format: Text
• Language: English
• Published: Alma Mater Studiorum - University of Bologna 2015
• Subjects: Logical frameworks; Certified Programming; Type-preserving Compilation; Lambda; Beluga*
• Online Access: https://dx.doi.org/10.6092/issn.1972-5787/5122; http://jfr.unibo.it/article/view/5122

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