Linear logical approximations

ract interpretation of programs relates the exact semantics of a programming language to an approximate semantics that can be effectively computed. We show that, by specifying operational semantics in a bottom-up, linear logic programming language – a technique we call substructural operational semantics (SSOS) – manifestly sound program approximations can be derived by simple and intuitive approximations of the logic program. As examples, we describe how to derive a simple alias analysis, 0CFA, and kCFA analysis from a substructural operational semantics of the relevant languages.

• Type: Conference
• Year: 2009
• Where: PEPM
• Authors: Robert J. Simmons, Frank Pfenning
• Keywords: Approximate Semantics, Exact Semantics, PEPM 2009, Software Engineering, Substructural Operational Semantics