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 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.