Substructural logics, such as linear logic and ordered logic, have an inherent notion of state and state change. This makes them a natural choice for developing logical frameworks that specify evolving stateful systems. Our previous work has shown that the so-called forward reasoning fragment of ordered linear logic can be used to give clear, concise, and modular specifications of stateful and concurrent features of programming languages in a style called Substructural Operational Semantics (SSOS).

This report is discusses two new ideas. First, I discuss a re-orientation of existing logics and logical frameworks based on a presentation of logic as a state transition system. Second, utilizing this transition-based interpretation of logic, I present a safety proof for the SSOS specification of a simple sequential programming language, and discuss how that proof can be updated as the language is extended with parallel evaluation and exception handling.

This report is derived from my thesis proposal, which was certified on July 7, 2010.

40 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu