Actualités du LIPN

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.

Le 28 novembre 2011, à 14h en salle B311, le séminaire LCR accueille Paolo Parisen Toldin (Bologne).

We present RSLR, an implicit higher-order characterization of the class PP of those problems which can be decided in probabilistic polynomial time with error probability smaller than 1/2. Analogously, a (less implicit) characterization of the class BPP can be obtained. RSLR is an extension of Hofmann’s SLR with a probabilistic primitive, which enjoys basic properties such as subject reduction and confluence. Polynomial time soundness of RSLR is obtained by syntactical means, as opposed to the standard literature on SLR-derived systems, which use semantics in an essential way.