Logic and interaction (6 – 10 February)

Talk list

Lectures

Invited talks

  • Michele Abrusci (Roma, Italy) and Paolo Pistone (Roma, Italy), Transcendental Syntax and Geometry of Interaction : Interplays between Logic and Philosophy.
    • Monday 6, 16:00
  • Dan Ghica (Birmingham, UK), A System-Level Semantics.

    Game semantics is a trace-like denotational semantics for programming languages where the notion of legal observable behaviour of a term is defined combinatorially, by means of rules of a game between the term (the "Proponent") and its context (the "Opponent"). In general, the richer the computational features a language has, the less constrained the rules of the semantic game. In this paper we consider the consequences of taking this relaxation of rules to the limit, by granting the Opponent omnipotence, that is, permission to play any move without combinatorial restrictions. However, we impose an epistemic restriction by not granting Opponent omniscience, so that Proponent can have undisclosed secret moves. We introduce a basic C-like programming language and we define such a semantic model for it. We argue that the resulting semantics is an appealingly simple combination of operational and game semantics and we show how certain traces explain system-level attacks, i.e. plausible attacks that are realizable outside of the programming language itself. We also show how allowing Proponent to have secrets ensures that some desirable equivalences in the programming language are preserved.

    • Thursday 9, 14:00
  • Kurt Ranalter (Bolzano, Italy), Abstract machines for argumentation.

    One of the most striking features of ludics is that it provides us with convenient tools for the modelling of interaction. As a consequence, ludics has been exploited to provide a framework for the modelling of dialogues. In this talk we shall address some of the issues that arise when one tries to model certain types of dialogues that occur frequently in the field of argumentation. We shall exploit that ludics' designs can be regarded as abstract Böhm trees and explain how the pointer interaction of the associated geometric abstract machine GAM relates to a notion of backtracking.

    • Friday 10, 14:00

Contributed talks

  • Michele Basaldella (RIMS, Japan), A gentle introduction to ludics.

    When one is interested in understanding the duality between syntax (proofs) and semantics (models) in logic, a primary obstacle is that proofs are finite and concrete objects, while models are infinite and abstract structures. Since proofs and models are so different by their nature, they hardly interact together. This lack of interaction between the two worlds prevents a deeper analysis of the relations between syntax and semantics.

    Ludics is a research program started by Girard aimed to explain various logical and computational phenomena from an interactive point of view. The universe of ludics consists of designs: partial and infinitary proofs in which the logical type-information has been almost erased. In this vast universe, both proofs and models can be homogeneously represented as designs. Moreover, since designs come from proofs, we can make them interact together via normalization (cut-elimination). This induces an orthogonality relation, based on the termination of the computation of the normal form, which allows to reconstruct the logical types, as bi-orthogonality-closed sets of designs.

    In this talk we introduce and discuss the basic concepts of ludics and show some completeness results for proofs.

    • Thursday 9, 15:30
  • Etienne Duchesne (Paris, France), MELL in a free compact closure.

    The categorical presentation of the standard model of the geometry of interaction --namely the free compact closure of sets and partial injections Int(PInj)-- fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.

    • Wednesday 8, 16:00
  • Pierre-Marie Pédrot (Paris 7, France), Double-glueing: refining models of linear logic through realizability.

    The double-glueing technique, designed by Hyland and Schalk, is a generalization of the underlying structure common to most models of linear logic. This process transforms constraintless models to finer ones, thanks to an orthogonality refinement that captures stricter notions of proofs and counter-proofs.

    This construction is at work in many models of LL and permits a nice factorization of the latter. In addition, it also sheds a new light upon polarization, relaxing the double-orthogonal closure of LL. This results in a better separation between exponentials and shifts.

    Actually, double-glueing seems to be a promising way to integrate dependent types and subtyping into linear logic, through realizability, instead of more direct syntactical approaches.

    • Thursday 9, 16:15
  • Christian Rétoré (Bordeaux, France), Du système F pour la sémantique et pour la pragmatique lexicale : application à quelques phénomènes linguistiques.

    Les grammaires catégorielles (Bar-Hillel, Lambek, Montague, Moortgat,..) associent à une analyse syntaxique une formule de la logique du premier ordre (ou d'ordre supérieur), en s'appuyant sur le codage de Church de la logique en lambda calcul simplement typé sur deux types : les entités et les valeurs de vérité.

    Linguistiquement, ce typage à la Church-Montague est très grossier: il ne permet pas d'imposer le type des arguments ("animé" pour le sujet de manger) ni de traiter des facettes ou d'une forme particulière de polysémie lexicale.
    On est donc amené à avoir au minimum plusieurs types de base correspondant à une sorte d'ontologie linguistique, et certaines opérations sont alors uniformes sur les types, comme la quantification, la conjonction.

    C'est pourquoi on utilise le système F de Jean-Yves Girard qui permet d'attribuer des types variables aux expressions. Le lexique associe à chaque mot le terme à la Montague qui exprime sa structure logique et argumentale ainsi que des termes qui permettent de le convertir d'un type à un autre si besoin, par exemple pour s'adapter au contexte. ("j'ai perdu mon livre" renvoie à l'objet physique et non au contenu informationnel)

    Nous expliquerons comment le système F produit, et uniquement lorsque c'est licite, des formules de la logique multisorte d'ordre supérieur qui rendent compte de ces constructions. Un raffinement linéaire du système F permet de gérer au niveau du typage certains types d'impossibilité, et nous parlerons de cette amélioration en cours.

    Précisons qu'il s'agit de construire des formules logiques représentant le sens des énoncés et non de définir leur référence ou leur vérité dans une situation donnée. Pour interpréter ce type d'énoncés complexes d'autres types de modèles sont sans doute mieux adaptés (ludique).

    L'idée qui sous-tend ce travail est que les termes expriment l'aspect purement sémantique du sens, tandis que les types qui sont flexibles sont plutôt déterminés par le contexte.

    • Friday 10, 15:30
  • Thomas Seiller (Chambéry, France), Graphs of Interaction .

    Graphs of Interaction are a generalization of the very first version of geometry of interaction defined by Girard in his article "Multiplicatives" by replacing permutations with directed weighted graphs. In this setting, it is possible to define a notion orthogonality, parametrized by a "measure" on cycles, by counting the cycles that appear when one plugs two graphs together. With such a notion of orthogonality, one can then construct a denotational model for multiplicative additive linear logic (MALL) and define a notion of truth.

    Moreover it can be shown that two particular choices of "measure" maps define either a combinatorial version of Girard's geometry of interaction in the hyperfinite factor (GoI5) or a slightly refined version of the older "Geometry of Interaction I" where orthogonality is defined by nilpotency. Thus, this framework gives a geometrical interpretation to GoI5's orthogonality (which is based on the determinant), and shows how one can relate this new construction with the first versions of geometry of interaction.

    • Wednesday 8, 16:45