Actualités du LIPN

[LIPN] [CNRS] [Université Paris 13]

To content | To menu | To search

Keyword - logique linéaire

Entries feed - Click here to abridge

Past posts

Monday 14 May 2012

Explicit substitutions at a distance, rewriting, and applications to the theory of lambda calculus

fr 

Monday 14 May 2012 at 02.00 PM — Seminars

Le 14 mai 2012, à 14h en salle B311, le séminaire LCR accueille Beniamino Accattoli (LIX).

In some works in collaboration with Stefano Guerrini and Delia Kesner I developed a new approach to explicit substitutions, arising from Linear Logic proof-nets. The idea is to design calculi mimicking closely the dynamics of the graphical cut-elimination rules. Proof-nets and terms have very different notions of locality: this fact induce non-local, "at a distance" rewriting rules on terms. Substitution calculi at a distance are half-way lambda calculus and typical explicit substitution calculi: they retain most of the simplicity of lambda calculus, keeping the subtleties and the finer evaluation of explicit substitutions. In a series of recent works (some of which are joint works with Delia Kesner, Luca Paolini or Ugo Dal Lago) I explored systematically the rewriting theory of these calculi. In the talk I will survey the problems I studied (confluence, preservation of strong normalization, sigma-equivalence, developments, solvability, factorization, standardization, residuals) and the results I obtained, showing how they provide new understandings of classical notions and results - and sometimes even new results - in the theory of lambda-calculus.

Monday 31 May 2010

Graphes d'interaction

fr 

Monday 31 May 2010 at 03.30 PM — Seminars

Le 31 mai 2010, à 15h30 en salle B311, le séminaire LCR accueille Thomas Seiller (IML, Aix-Marseille 2).

Je présenterai une sémantique localisée du fragment multiplicatif de la logique linéaire (MLL) où les preuves sont représentées par des graphes. Cette sémantique, inspirée des derniers travaux de J.-Y. Girard, se révèle être une version combinatoire de la géométrie de l’interaction dans le facteur hyperfini. Elle permet en particulier de mettre en rapport ces récents développements et les réseaux de preuves, les sémantiques de jeu ou la ludique. Je discuterai également d’une généralisation au fragment multiplicatif-additif de la logique linéaire (MALL).

Monday 12 April 2010

La sémantique relationnelle de la logique linéaire est-elle injective?

fr 

Monday 12 April 2010 at 01.30 PM — Seminars

Le 12 avril 2010, à 13h30 en salle D214 (attention à la salle inhabituelle !) le séminaire LCR accueille Daniel de Carvalho (LIPN).

Pour un certain fragment de la logique linéaire, la relation d’équivalence sur les preuves induite par l’élimination des coupures coïncide avec celle induite par le modèle relationnel basé sur les multi-ensembles.

Monday 11 January 2010

Finite automata and regular fixed point formulas in muMALL

fr 

Monday 11 January 2010 at 03.30 PM — Seminars

Le 11 janvier 2010, à 15h30 en salle B311, le séminaire LCR accueille David Baelde (University of Minnesota, USA).

We present muMALL, an extension of multiplicative additive linear logic with least and greatest fixed points, and illustrate its expressiveness through the model-checking problem of non-deterministic finite automata inclusion.

We consider encoding automata as least fixed points in muMALL, and use its general induction scheme to reason about them. We provide a coinductive characterization of inclusion that yields a natural bridge to proof-theory. This yields a completeness theorem, but can also be generalized to the fragment of "regular formulas", obtaining new insights about inductive theorem proving and cyclic proofs in particular.

Monday 23 March 2009

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

fr 

Monday 23 March 2009 at 02.00 PM — Seminars

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.

Tuesday 2 December 2008

Soutenance de thèse de Vincent Atassi

fr 

Tuesday 2 December 2008 at 04.00 PM — PhD & Habilitations defends

Bonjour à tous, j’ai le plaisir de vous inviter à la soutenance de ma thèse intitulée « Typage et Réduction Optimale pour le lambda-calcul dans les variantes de la Logique Linéaire pour la complexité implicite ».

La soutenance aura lieu salle B311 du LIPN (Institut Galilée) à Paris-13 Villetaneuse le mardi 2 décembre à 16h00 (plan d’accès) et le jury sera composé de :

  • Patrick Baillot, CNRS/ENS Lyon, Directeur
  • Christophe Fouqueré, Université Paris 13, Examinateur
  • Ian Mackie, CNRS/Ecole Polytechnique, Rapporteur
  • Simone, Martini, Università di Bologna, Rapporteur
  • Virgile Mogbil, Université Paris 13, Examinateur
  • Laurent Regnier, Université Aix-Marseille 2, Examinateur
  • Simona Ronchi Della Rocca, Università di Torino, Examinatrice
  • Jacqueline Vauzeilles, Université Paris 13, Co-Directrice

Vous êtes bien sûr également conviés au pot qui suivra. Une page regroupant les informations sur la soutenance et contenant une version préliminaire du manuscrit est disponible : http://www-lipn.univ-paris13.fr/~atassi/soutenance/

Continue reading...

Monday 29 September 2008

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

fr 

Monday 29 September 2008 at 01.30 PM — Seminars

The inaugural meeting of the 2008/2009 GdT "Logique et Programmation" will take place on

   Monday, 29 September 2008,
   at 1:30 pm, in room B311.

We will listen to a talk by Paolo Di Giamberardino (ATER LIPN - IUT Villetaneuse), who will tell us about his proof nets with jumps for multiplicative additive linear logic.

Tuesday 11 March 2008

Soutenance d'habilitation de Patrick Baillot

fr 

Tuesday 11 March 2008 at 02.00 PM — PhD & Habilitations defends

Bonjour, j’ai le plaisir de vous inviter à ma soutenance d’habilitation à diriger les recherches. Elle aura lieu le mardi 11 mars 2008, à 14h, à l’Institut Galilée, Amphi Euler Université Paris 13 (Villetaneuse) et sera suivie d’un pot qui aura lieu au LIPN.

Les informations pratiques (accès...) seront actualisées sur ma page.

Amicalement, Patrick Baillot

Continue reading...

Monday 11 February 2008

Workshop on Implicit Computational Complexity

en 

Monday 11 February 2008 at 12.00 PM — Conferences

Implicit Computational Complexity

Implicit Computational Complexity (ICC) has emerged from various propositions to use logic and formal methods like types, rewriting systems, interpretations... to provide languages for complexity-bounded computation, in particular for polynomial time computing.

It aims at studying the computational complexity of programs without refering to a particular machine model and explicit bounds on time or memory, but instead by relying on programming or logical disciplines that imply complexity properties. Several approaches have been explored for that purpose, like restrictions on primitive recursion, lambda calculus, types, linear logic, rewriting systems .... They originally mostly came from the functional programming paradigm, but imperative programming is now also addressed. Two objectives of ICC are:

  • on the one hand to find natural implicit logical characterizations of functions of various complexity classes,
  • on the other hand to design criteria usable for the static verification of programs complexity. In particular the latter goal requires characterizations which are flexible enough to validate commonly used algorithms.

Finding out more

The home page of this workshop supported by the NO-CoST ANR project is online.