|
|
|
|
Dernière mis à jour : 18/01/2010
Laboratoire PPS
Université Paris Diderot - Paris 7
Case 7014
75205 PARIS Cedex 13
Tél : +33-1 44 27 53 05
Je suis chercheur au CNRS, membre du laboratoire Preuves, Programmes et Systèmes (PPS).
Je m'intéresse à la logique, et plus particulièrement à la théorie de la démonstration, dans les rapports qu'elle entretient avec l'informatique théorique à travers l'isomorphisme de Curry-Howard. On trouvera dans ce texte une présentation générale de mes travaux.
Je me suis occupé du projet Geocal de l'ACI Nouvelles Interfaces des Mathématiques, de septembre 2003 à septembre 2006.
Je suis responsable du projet blanc ANR Curry-Howard pour la concurrence CHOCO. Ce projet vient de commencer. Voici un résumé du projet et une présentation plus complète, extraits du dossier de candidature.
Je suis membre du groupe de travail Geocal du GDR Informatique Mathématique.
On touvera ici mes notes de cours et des feuilles de TD pour la partie Domaines du cours Modèles des langages de programmation 2-2, dans le master MPRI. Attention : ces notes sont en cours de rédaction. La version en ligne n'est donc ni complète, ni définitive !
Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science, Cambridge University Press. 1993. pdf.
On strong stability and higher-order sequentiality. Logic in Computer Science. Ninth Symposium on Logic in Computer Science, Paris, 1994. IEEE. 1994. pdf.
Sequentiality in an extensional framework. Information and Computation, Academic Press. 1994. pdf.
Projecting sequential algorithms on strongly stable functions. Annals of Pure and Applied Logic, North Holland. 1996. pdf.
Anatomy of an extensional collapse. 1997. Unpublished manuscript. pdf.
A relative definability result for strongly stable functions and some corollaries. Information and Computation, Academic Press. 1999. pdf.
Parallel and serial hypercoherences. Theoretical Computer Science, Elsevier. 2000. pdf.
On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic, North Holland. 2000. pdf.
On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, North Holland. 2001. pdf.
On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, Cambridge University Press. 2002. pdf.
A completeness theorem for symmetric product phase spaces. Journal of Symbolic Logic, Association for Symbolic Logic. 2004. pdf.
The differential lambda-calculus. Theoretical Computer Science, Elsevier. 2004. pdf.
Web based models of linear logic. Slides of my talk at WoLLIC'04, Fontainebleau. 2004. pdf.
Finiteness spaces. Mathematical Structures in Computer Science, Cambridge University Press. 2005. pdf.
Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, Elsevier. 2006. To appear. pdf.
Differential interaction nets. Theoretical Computer Science, Elsevier. 2006. To appear. pdf.
Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms. Logical Approaches to Computational Barriers. Second Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006. Lecture Notes in Computer Science. Springer Verlag. 2006. Extended abstract. pdf.
Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms. 2006. Long version. pdf.
Embedding the pi-calculus in differential interaction nets. Slides of my talk at the conference Computability in Europe 2006 (CiE 2006), Swansea. 2006. pdf.
Embedding the Finitary Pi-calculus in Differential Interaction Nets. 2006. Electronically published proceedings. Available here.
On differential interaction nets and the pi-calculus. 2006. HAL technical report ccsd-00096280, version 1. Available here.
On finiteness spaces and extensional presheaves over the Lawvere theory of polynomials. 2007. Accepted for publication in the Journal of Pure and Applied Algebra. pdf.
Not enough points is enough. 2007. Computer Science Logic. pdf.
Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. 2007. CONCUR, conference short version. pdf.
Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. 2007. Slides of a talk given at University Roma III, the 16th of April. pdf.
A relational model of a parallel and non-deterministic lambda-calculus. 2008. Accepted at LFCS 09. .
Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. 2008. Submitted for publication. Long version of the CONCUR paper. ps, pdf.
On probabilistic coherence spaces. 2008. PPS and CHOCO technical report. Submitted for publication. pdf.
Acyclic Solos and Differential Interaction Nets. 2008. PPS and CHOCO technical report. Submitted for publication. pdf.
The Scott model of Linear Logic is the extensional collapse of its relational model. 2009. PPS and CHOCO technical report, HAL hal-00369831, submitted for publication. pdf.
A finiteness structure on resource terms. 2010. PPS and CHOCO technical report, HAL, submitted for publication. pdf.