Copenhagen Programming Language Seminar

Substructural Operational Semantics

Frank Pfenning
Carnegie Mellon University

Thursday, April 17th, 2008, 15:15-16:15
IT University, Rued Langgaardsvej 7 , 2300 Copenhagen, Auditorium 4


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 how it differs from prior proposals, specifically, the LolliMon fragment of the concurrent logical framework (CLF).

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]

Scientific host: Carsten Schürmann. Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org