Towards Provably Correct Code Generation via Horn Logical Continuation Semantics

Abstract. Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming language semantics, particularly Horn logical semantics, and partial evaluation. We show that the definite clause grammar (DCG) notation can be used for specifying both the syntax and semantics of imperative languages. We next show that continuation semantics can also be expressed in the Horn logical framework.

• Type: Conference
• Year: 2005
• Where: PADL
• Authors: Qian Wang, Gopal Gupta, Michael Leuschel
• Keywords: Logical Semantics, PADL 2005, Programming Language Semantics, Programming Languages, Provably Correct