Séminaire, Dec. 4, 2014

Cette réunion se tiendra à Marseille, plus précisément à Luminy (notez au passage les horaires inhabituels).

Pour aller à Luminy, voici un lien, et voici un plan du campus.

Nous serons le matin dans l'amphi 1 du bâtiment A : c'est le rectangle bleu qui porte le numéro 6 sur le plan. Après avoir déjeuné dans une bonne auberge, nous serons l'après-midi dans les locaux du labo I2M, qui se trouve dans la partie CNRS du bâtiment TPR2: c’est le rectangle orange numéro 5.


11:00 – 12:30
Paul Levy (Birmingham University)

We describe a framework for game semantics combining operational and denotational accounts. A game is a bipartite graph of “passive” and “active” positions, or a categorical variant with morphisms between positions.

The operational part of the framework is given by a labelled transition system in which each state sits in a particular position of the game. From a state in a passive position, transitions are labelled with a valid O-move from that position, and take us to a state in the updated position. Transitions from states in an active position are likewise labelled with a valid P-move, but silent transitions are allowed, which must take us to a state in the same position.

The denotational part is given by a “transfer” from one game to another, a kind of program that converts moves between the two games, giving an operation on strategies. The agreement between the two parts is given by a relation called a “stepped bisimulation”.

The framework is illustrated by an example of substitution within a lambda-calculus.

(Joint work with Sam Staton)

14:00 – 15:00
Guillaume Geoffroy (ENS Paris)

Classical realizability is a rewrite of Kleene's realizability in order to make it compatible with classical reasoning, following the discovery by T. Griffin of a connection between classical reasoning and control operators. J.-L. Krivine used classical realizability semantics to construct novel models of standard set theory (ZF).

I will explain how classical realizability semantics work, how to construct classical realizability models of ZF, and how they differ from forcing models. Notably, each classical realizability model contains a characteristic boolean algebra ∇2, of mysterious structure and weird cardinality. Specifically, I will focus on the model of threads, which showcases these differences.

15:30 – 16:30
Kazushige Terui (Kyoto University)

Hypersequent calculus, introduced by Arnon Avron, is an extension of the ordinary sequent calculus that deals with disjunctions of sequents. Historically it has been a tool for studying intermediate logics and many-valued logics (so-called fuzzy logics), but it is interesting in its own right as a proof system with a well-behaved cut-elimination procedure.

In this talk, I will discuss some aspects of hypersequents, that could be hopefully meaningful to those who are not interested in fuzzy logics at all. The topics include:

  • Brouwer's fixed point theorem and cut-elimination: a potential link.

  • Algebraic cut-elimination a la Maehara and Okada: success and failure.

  • Takeuti-Titani's density rule: elimination and algebraic interpretation.