A dual calculus for unconstrained strategies

Alexis Goyet

(University Paris Diderot (Paris 7))

The aim of the lambda lambda-bar calculus is to represent as faithfully as possible the structure of non-deterministic, non-innocent, non-visible strategies in game semantics. Non-innocent strategies have been shown to model functional languages extended with references. The typical approach is to model the purely functional fragment with innocent strategies, to which a "memory-cell" strategy is added. Instead, our starting point is a simple concrete syntax of finite strategies, which are inherently non-innocent. This approach is syntax driven, and the resulting language is a dualization of the lambda calculus. A new binder, the lambda-bar, names arguments which have been passed to the environment (whereas the lambda names arguments which have been received). This makes explicit the act of answering a function call, and allows this answer to change over time, granting the power of effects.
Wednesday 27th November 2013, 16:00
Far-134 (video conferencing room)
Department of Computer Science