Actualités du LIPN

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.

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

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.