vincent atassi


This page contains documents, articles and programs by Vincent Atassi.

Intérêts de recherche

Logique linéaire, programmation fonctionnelle, Réduction optimale, inférence de type.

Document(s)

Manuscrit préliminaire de thèse, version de Novembre 2008: Typing and Optimal reduction for lambda-calculus in variants of Linear logic for Implicit computational complexity

Avec Patrick Baillot et Kazushige Terui : Verification of Ptime reducibility for system F terms via Dual Light Affine Logic ,
in the Proceedings of Computer Science Logic 2006 (CSL'06), volume 4207 of LNCS, pp.150-166. © Springer.

Rapport de stage master 2 recherche au MPRI de l'été 2005 : Sous-typage et coercitions dans ELL


Programme(s)

Programme caml d'inférence de type de logique linéaire élémentaire en lambda calcul, à faire marcher avec un solveur (glpsol par exemple)
Glpsol peut être trouvé à http://www.gnu.org/software/glpk/glpk.html

Programme caml d'inférence de type Dual Light Affine Logic (DLAL), à faire marcher avec un solveur (glpsol par exemple)
Glpsol peut être trouvé à http://www.gnu.org/software/glpk/glpk.html

Programme caml de génération de termes pour le typage DLAL. On génère (avec ou sans coercitions) des termes représentants un polynomes donné en entrée.