| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 9656009 | Electronic Notes in Theoretical Computer Science | 2005 | 23 Pages |
Abstract
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we present an approach to provably correct compilation based on Horn logical semantics of programming languages and partial evaluation. We also show that continuation semantics can be expressed in the Horn logical framework, and introduce Definite Clause Semantics. We illustrate our approach by developing the semantics for the SCR specification language, and using it to (automatically) generate target code in a provably correct manner.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Qian Wang, Gopal Gupta,