Detail

Substructural Operational Semantics

Substructural operational semantics (SSOS) is a formalism for the modular
specification of programming languages. It employs techniques
from substructural logics and type theories (ordered, linear, affine,
and strict) to give elegant, concise, and modular specifications.
Interestingly, we can create a taxonomy of language features based
on which kind of structural properties are necessary to define an
operational semantics.

When the substructural logic itself is endowed with an operational
interpretation via forward and backward chaining proof search,
an SSOS specification is directly executable. We sketch this
operational interpretation and discuss some open questions
in this area.

Time permitting we will also discuss some ongoing research which
aims at deriving program analysis algorithms and their implementations
by abstraction from an SSOS specification. It appears that equality
reasoning plays a crucial role in this process, and we speculate
how this might be integrated in a way that is both logically and
operationally adequate.

[This talk presents joint work with Rob Simmons]