Séminaire, 4 décembre 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.
Programme
- 11:00 – 12:30
-
Paul Levy (Birmingham University)Invited talk: Transition systems over games
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)Invited talk: Some topics on hypersequents
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.
