Towards a non-commutative logic of effects

Noam Zeilberger (Laboratoire PPS, Université Paris 7 - Denis Diderot)

Info

Date	3rd December 2010 (week 8, Michaelmas Term 2010)
Time	14:00
Place	Lecture Theatre B

Abstract

I will present work-in-progress (with Jonas Frey and Paul-André Melliès) aimed at establishing closer links between the theory of
computational effects and linear logic in the broad sense. Starting from an analogy between polarity and "Isbell duality", I will describe
a new categorical interpretation of (polarized, non-commutative) linear logic, and suggest its potential applications for describing
and reasoning about programs with side effects. In particular, I will consider as a case study Reynolds' equation "intvar = intexp &
intacc", defining an integer variable (in the Forsythe language) as the intersection of an integer expression and an integer acceptor.