Sciweavers

Share
ICFP
2003
ACM

Compiler implementation in a formal logical framework

9 years 11 months ago
Compiler implementation in a formal logical framework
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present proach based on the use of higher-order abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of rewrite rules that are written in the language of formal mathematics. In addition, the logical framework guarantees the preservation of scoping, and it automates many frequently-occurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a general-purpose language like ML, in part because of automation, and also because the framework provides extensive support for examination, validation, and debugging of the compiler transformations. The paper is organized around a case study, using...
Jason Hickey, Aleksey Nogin, Adam Granicz
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2003
Where ICFP
Authors Jason Hickey, Aleksey Nogin, Adam Granicz
Comments (0)
books