Actualités du LIPN - Tag - GdT LogProg

La décidabilité de MELL et les réseaux de Petri

damiano — Monday 8 March 2010

Le 8 mars 2010, à 15h30 en salle B311, Paulin Jacobé de Naurois (LIPN) animera une séance du groupe de travail "Logique et Programmation".

La décidabilité de MELL et les réseaux de Petri.

Concurrent processes as (wireless!) proof nets

damiano — Monday 8 March 2010

Le 8 mars 2010, à 13h30 en salle B311, Virgile Mogbil (LIPN) animera une séance du groupe de travail "Logique et Programmation".

We present a proofs-as-programs correspondence between linear logic and process calculi that handles non-deterministic behaviours. The proof language is that of wireless proof nets, i.e. multiplicative proof nets with sets of cut formulas instead of cut wires. A correspondence is established between proof structures and pi-calculus terms under an interfacing condition. Correctness criteria for proofs induce a type system for processes where typing a term consists in typing some of its possible determinisations in standard sequent calculus. Generalized cut-elimination in proof nets is shown to correspond to deadlock-avoiding execution. (With Emmanuel Beffara - IML)

Virgile Mogbil : TBA

damiano — Monday 25 January 2010

Le 25 janvier 2010, à 13h30 en salle B311, Virgile Mogbil (LIPN) animera une séance du groupe de travail "Logique et Programmation".

Développement de Taylor entre syntaxe et sémantique

damiano — Monday 14 December 2009

La prochaine séance du GdT "Logique et Programmation" sera animée par Christine Tasson (PPS, Paris 7).

L’analogie entre la linéarité au sens informatique et la linéarité au sens mathématique est au cœur de la logique linéaire. D’ailleurs, elle a été récemment étendue par un opérateur différentiel permettant d’approcher les preuves par des représentations linéaires. Grâce à ces considérations, Ehrhard et Regnier ont introduit des syntaxes différentielles. Ils ont aussi montré l’existence d’une formule de Taylor syntaxique qui permet de simuler des termes par des séries d’approximations obtenues grâce à l’opérateur différentiel.

Dans un premier temps, je présenterai la formule de Taylor syntaxique. Nous verrons comment traduire les réseaux de la logique linéaire dans les réseaux différentiels. Ensuite nous verrons que les termes résultant de cette traduction possèdent une certaine uniformité.

Dans un second temps, je présenterai les aspects sémantiques qui ont mené à l’introduction de l’opérateur différentiel. Nous verrons comment, en partant du modèle relationnel, on peut construire un modèle dans lequel les types sont interprétés par des espaces vectoriels topologiques et les programmes par des fonctions développables en séries de Taylor.

Où et quand : B311, 14/12/2009, 13h30

Développement de Taylor entre syntaxe et sémantique

damiano — Monday 23 November 2009

La prochaine séance du GdT "Logique et Programmation" sera animée par Christine Tasson (PPS, Paris 7).

A Relational Model of Lambda Calculus, and Beyond (recent developments)

damiano — Monday 16 November 2009

For this first meeting of the new season of the GdT "Logique et Programmation" we will have Giulio Manzonetto (LIPN).

In this talk, we build a categorical model D of lambda calculus living in a category of sets and relations (relational semantics).

We will characterize the equational theory of this model, and show that it satisfies interesting algebraic properties that make it suitable for dealing with non-deterministic and parallel extensions of lambda calculus.

Unlike most traditional approaches, our way of interpreting non-determinism does not require any additional powerdomain construction: we show that our model provides a straightforward semantics of non-determinism (may convergence) by means of `unions' of interpretations as well as of `parallelism' (must convergence) by means of a binary, non-idempotent, operation available on the model, which is related to MIX rule of Linear Logic.

We describe the interpretation of this parallel and non-deterministic calculus in our model and show that this interpretation is sensible with respect to our operational semantics: a term converges if, and only if, it has a non-empty interpretation.

If time permits, we will sketch an interpretation of the resource lambda calculus in D.

Groupe de travail "Logique et Programmation": Paolo Di Giamberardino

damiano — Monday 23 March 2009

The next meeting of the GdT "Logique et Programmation", now officially sponsored by the ANR project Complice, will take place on

Monday, 23 March 2009,
at 2:00 pm, in room B311.

We will listen to a talk by Paolo Di Giamberardino (ATER LIPN - Institut Galilée), who will tell us how his approach of using jumps in linear logic proof nets can be extended to the exponentials.

Groupe de travail "Logique et Programmation": Damiano Mazza

damiano — Monday 12 January 2009

The next meeting of the GdT "Logique et Programmation" will take place on

Monday, 12 january 2009,
at 2:00 pm, in room B311.

We will listen to yet another talk by Damiano Mazza (LIPN), who will tell us about homotopy for rewriting systems and event structures.

Groupe de travail "Logique et Programmation": Amir Ben-Amram

damiano — Monday 24 November 2008

The next meeting of the GdT "Logique et Programmation" will take place on

Monday, 24 November 2008,
at 1:30 pm, in room B311.

We will listen to a talk given by Amir Ben-Amram, invited researcher from the School of Computer Science at the Academic College of Tel-Aviv Yaffo, who will tell us about his latest ideas regarding size-change termination.

Groupe de travail "Logique et Programmation": Damiano Mazza

damiano — Monday 3 November 2008

The next meeting of the GdT "Logique et Programmation" will take place on

Monday, 3 November 2008,
at 3:30 pm, in room B311.

We will listen to the second part of the talk started last time by Damiano Mazza (LIPN), about stratified parity spaces as a denotational semantics for linear logic by levels.