A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

Yuting Wang, Gopalan Nadathur

We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transfor…