Type safety for substructural specifications: preliminary results (CMU-CS-10-134)

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.