Institut de Mathématiques de Luminy

SÉMINAIRES 2012
Logique et Interactions

Organisateur :
Emmanuel Beffara (tél. 04 91 26 96 35)
Lieu : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.

logo PPS

jeudi 20 décembre
Alexis Goyet
(PPS, Paris 7)
A dual calculus for unconstrained strategies

Webpage : http://www.pps.univ-paris-diderot.fr/~agoyet/

Abstract: The aim of the λ λ-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.
The resulting language is a dualization of the λ-calculus. A new binder, the λ-bar, names arguments which have been passed to the environment (whereas the λ 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.


Pierre-Marie Pédrot

jeudi 29 novembre
Pierre-Marie Pédrot
(LIP, ENS Lyon)
"Ça d
épend, ça dépasse"
ou une monade d
épendante de contrôle délimité

Webpage : http://perso.ens-lyon.fr/pierremarie.pedrot/

Résumé : Les continuations délimitées présentent de nombreux avantages par rapport aux continuations classiques, l'un des plus notables étant la présence d'une opération permettant d'appliquer localement les effets. Ce gain d'expressivité repose sur un raffinement des types de la CPS habituelle.
À travers une traduction CPS délimitée d'un calcul avec inductifs et élimination dépendante, nous montrerons que cette monade connaît elle-même une généralisation intéressante. Certains opérateurs de contrôle bien connus y prennent des types enrichis inattendus.
Enfin, guidés par la logique linéaire polarisée, nous présenterons une extension naturelle à des types infinitaires, qui permet d'exprimer certains comportements de dépolarisation propres à la logique linéaire, le plus notable étant la commutation non-ordonnée a priori entre tenseur et double négation.


Clément Aubert

jeudi 22 novembre
Clément Aubert
(LIPN, Univ. Paris 13)
Caractérisation de co-NL par l'action d'un groupe

Webpage : http://lipn.univ-paris13.fr/~aubert/

Résumé : Girard, dans Normativity in Logic (2011), propose un emploi innovant de la Géométrie de l'Interaction (GdI) dans le facteur hyperfini pour caractériser des classes de complexité. Ce papier étant très technique et parfois allusif, nous proposons avec Thomas Seiller (LAMA - Université de Savoie) une relecture des résultats qu'il présente. En allégeant et simplifiant certaines définitions et critères, en introduisant un modèle de calcul innovant (les machines à pointeurs non-déterministes), nous parvenons à prouver de nouveau que co-NL peut-être caractérisé par l'action du groupe des permutations finies sur une algèbre de von Neumann.


University of Manchester Crest

jeudi 25 octobre
Hugh Steele
(Univ. Manchester)
Some results for linear logic full completeness

Abstract: Many full completeness theorems have been established for fragments of linear logic since the notion was first defined by Samson Abramsky and Radha Jagadeesan in their 1992 paper. For the most part, these results are obtained on a case-by-case basis: the subject of each proof is precisely one category.
In this talk it is shown that the Hyland-Tan double glueing construction can transform all tensor-generated compact closed categories with finite biproducts into fully complete models of unit-free MLL. The arguments employed are based around considering the combinatorics behind the construction using standard linear algebra. It is also discussed how another double glueing construction may be able to create similar categories satisfying unit-free MALL full completeness.


vendredi 14 septembre
en l'honneur de Jean-Yves Girard
Amphi Herbrand

Pierre-Louis Curien


à 11h30

Pierre-Louis Curien
(PPS, Paris 7)
Syntaxes pour calculs de s
équents

Webpage : http://www.pps.univ-paris-diderot.fr/~curien/

Michele Abrusci


à 10h30

Michele Abrusci
(Rome 3, La Sapienza)
Interactions entre logique, philosophie
et math
ématiques

Webpage : http://host.uniroma3.it/dipartimenti/filosofia/personale/schdado2.htm


logo la sapienza

jeudi 13 septembre
à 14h

Marco Caminati
(Rome, La Sapienza)
Software design themes in mathematical proving

Webpage : https://sites.google.com/site/marcocaminati/

Abstract: Concrete formalization of mathematics poses issues of software engineering flavor generally overlooked when writing standard mathematical papers, like choosing concise, convenient and maintainable encodings for the objects in the chosen foundations, modularising and cleaning the interface of lemmas so as to favour code reusing, hunting for hidden and superfluous assumptions. These various steps are often mutually related, so that cyclically iterating between them can lead to the discovery of versions of existing results which are stronger or somehow carrying more information. I will discuss this approach based on the concrete formalization in the Mizar system of cornerstone results of classical logic.


Tom Hirschowitz

jeudi 22 mars
à 11h

Tom Hirschowitz
(LAMA, Chambéry)
A construction of operational and game semantics
for CCS

Webpage : http://www.lama.univ-savoie.fr/~hirschowitz/

Abstract: We introduce a new algebraic structure called playground. From any playground D we construct (1) a language SD and its operational semantics (a labelled transition system (lts)) and (2) a game (or presheaf) semantics. We then construct an lts GD for strategies in the game semantics, and a translation from terms to strategies, which is shown to be a strong, functional bisimulation. We consider a particular playground, DCCS, which makes previous work with Pous on Milner's CCS an instance of our framework. Finally, we exhibit a functional, weak bisimulation of standard CCS into SDCCS, which shows that the game semantics of CCS given with Pous is a weak bisimulation. Weakness of bisimulation here is not w.r.t. synchronisation, but w.r.t. a kind of administrative reductions close to heating in the chemical abstract machine.

Liste des séminaires de l'année ...
[2002] [2003] [2004] [2005] [2006] [2007] [2008] [2009] [2010] [2011]

EL, le 13 décembre 2012