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 |
| Language: | English |
| Published: |
University of Bologna
2015-12-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/5122 |