Actualités du LIPN

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.

Le 23 avril 2012, à 14h en salle B311, le séminaire LCR accueille Paolo Parisen Toldin (Bologne).

Contrary to ICC standard approach, we present a small WHILE language characterizing the class PP.

The main problem concerning the imperative approach is to understand how informations/values flow throw variables in a program.

In literature are well known many works that have polytime soundness but just few of them (using the imperative paradigm) are able to give a polytime completeness.

Our system, MAL0 (Multiplied, Affine, Linear, 0 dependeces ), is sound and complete. Moreover, our system can be used also to check if a program is running in probabilistic polytime (can be easily restrict to just polytime soundness). We claim that, contrary to works found in literature, our system is able to certify a program in polytime.

This is a joint work in progress with Jean-Yves Moyen.

Le 19 mars 2012, à 14h en salle B311, le séminaire LCR accueille Arnaud Spiwack (PiR2).

Herbelin & Curien’s μ language gives a syntax to classical sequent calculus while leaving contraction and weakening implicit (more precisely dealt with by variables), like one would expect of a programming language. I will present an extension of H&C’s μ for linear sequent calculus which still relies on variables for contraction and weakening. I will then proceed and show how to give it a hint of dependent types, though I must confess there are some troubles there.

Le 5 mars 2012, à 14h en salle B311, le séminaire LCR accueille Thibaut Balabonski (PPS).

Les stratégies de réduction avec partage fournissent des pistes pour l’évaluation efficace des programmes fonctionnels. En quarante ans, ces modes de réduction ont été définis dans des cadres formels variés, hétérogènes et parfois complexes, utilisant par exemple des clôtures, des graphes, ou des transformations de programmes.

Je présenterai un système de récriture simple et expressif dans lequel nombre de ces approches peuvent être unifiées, analysées, et comparées. On étudiera en particulier quelques avatars de la réduction pleinement paresseuse (dont une des variantes est implémentée dans le compilateur GHC) et on précisera en quoi ces différents systèmes sont équivalents. Enfin, une utilisation judicieuse d’une transformation de programmes classique (le lambda-lifting) permettra d’établir un lien entre la pleine paresse et la réduction optimale des systèmes du premier ordre.. Ce lien sera suffisamment fort pour permettre le transfert de propriétés non triviales du premier ordre vers le lambda-calcul.