Programming type-safe transformations using higher-order abstract syntax
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...
Main Authors: | , , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Alma Mater Studiorum - University of Bologna
2015
|
Subjects: | |
Online Access: | https://jfr.unibo.it/article/view/5122 https://doi.org/10.6092/issn.1972-5787/5122 |