20 décembre 2012, 11:00 : Séminaire

Alexis Goyet (PPS, Paris 7), A dual calculus for unconstrained strategies

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.

29 novembre 2012, 14:00 : Séminaire

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

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.

22 novembre 2012, 14:00 : Séminaire

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

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.

15 novembre 2012

Séminaire Chocola et réunion du projet ANR Récré.

25 octobre 2012, 14:00 : Séminaire

Hugh Steele (Manchester), Some results for linear logic full completeness

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.

13 septembre 2012, 14:00 : Séminaire

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

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.

22 mars 2012, 11:00 : Séminaire

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

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.

19 janvier 2012, 11:00 : Séminaire

Marc Bagnol (IML), Cycles et trace

Dans «Syntaxe transcendantale» de JY Girard, l'interaction entre deux objets ("épistates") est mesurée à l'aide d'une formule basée sur la trace de l'intersection de deux projecteurs. On verra qu'on peut en fait voir cette formule comme une façon de compter les cycles qui se forment lors du "branchement" de deux graphes.

12 janvier 2012

Journée inaugurale du projet ANR Récré.