Dernière mise à jour : 5/02/2017
Université Paris Diderot - Paris 7
75205 PARIS Cedex 13
Tél : +33-1 57 27 92 17
Adresse physique : Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris. Bureau 3012.
I am a CNRS senior researcher and deputy director of the laboratory Institut de Recherche en Informatique Fondamentale (IRIF).
I am interested in logic, and mainly in Proof Theory and its connections with Computer Science through the Curry-Howard Correspondence. A general presentation of my work: texte (in French).
A categorical semantics of constructions. Logic in Computer Science. Third Symposium on Logic in Computer Science, Edinburgh, 1988. IEEE. 1988. pdf.
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 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.
On probabilistic coherence spaces. 2008. PPS and CHOCO technical report. To appear in Information and Computation. pdf.
Acyclic Solos and Differential Interaction Nets. 2008. PPS and CHOCO technical report. Paru dans Logical Methods in Computer Science 6(3), 2010. pdf.
The Scott model of Linear Logic is the extensional collapse of its relational model. 2009. Theoretical Computer Science 424: 20-45 (2012). pdf.
A relational semantics for parallelism and non-determinism in a functional setting. Annals of Pure and Applied Logic, Elsevier. 2009. To appear in 2011. pdf.
Resource Combinatory Algebras. 2010. MFCS 2010. pdf.
A Finiteness Structure on Resource Terms. 2010. LICS 2010. pdf.
Exponentials with Infinite Multiplicities. 2010. CSL 2010 (long version, with proofs in an appendix). pdf.
Categorical Models for Simply Typed Resource Lambda-Calculus. 2010. MFPS 2010. pdf.
Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. Information and Computation, Elsevier. 2010. 208(6), pp. 606-633. pdf.
Full Abstraction for Resource Calculus with Tests. 2011. Accepted at CSL 2011, Bergen. pdf.
A Convenient Differential Category. Cahier de Topologie et Géométrie Différentielle Catégoriques, . 2011. To appear. pdf.
A semantical introduction to differential linear logic. 2011. Submitted for publication. This paper contains an existence condition for anti-derivatives in categorical models of differential linear logic. Last update: Feb 2016. pdf.
Resource lambda-calculus: the differential viewpoint. 2011. Slides of an invited talk at CSL 2011, Bergen. Anti-derivatives are alluded to in this talk as well. pdf.
The Computational Meaning of Probabilistic Coherence Spaces. 2011. Accepted at LICS 2011. pdf.
An application of the extensional collapse of the relational model of linear logic. 2012. Submitted. pdf.
About the extensional collapse of Rel. 2012. Slides of a talk given at LI 2012 (CIRM, Marseille). pdf.
CCS for trees. 2013. Submitted for publication. pdf.
CCS for trees. 2013. Slides of a talk given at the workshop LOCALI 2013 (Beijing). pdf.
A new correctness criterion for MLL proof nets. 2014. Accepted at LICS'14. This criterion was first published by C. Rétoré in TCS 294(3):473-488, 2003. I rediscovered it independently (my presentation is slightly more general) and I am convinced that it is worth being further studied. pdf.
Sémantique des preuves et des programmes. 2014. Transparents d'un exposé didactique donné à la journée d'inauguration de la Fédération d'informatique fondamentale de Paris Diderot, le 7/2/2014. pdf.
Sémantique quantitative et qualitative de PCF. 2014. Transparents d'un exposé invité aux journées du GT GEOCAL du GDR Informatique Mathématique, le 24 mars 2014. pdf.
Call-By-Push-Value from a Linear Logic point of view. 2015. Accepted at ESOP 2016 (long version, with proofs). pdf.
Full abstraction for probabilistic PCF. 2015. Submitted for publication. pdf.
On Classical PCF, Linear Logic and the MIX rule. 2015. CSL 2015, Berlin. pdf.
A dendroidal process calculus. 2015. Submitted for publication. pdf.
Call-By-Push-Value from a Linear Logic point of view. 2016. Accepted at ESOP 2016. pdf.
Effects in Call-By-Push-Value, from a Linear Logic point of view. 2016. Submitted for publication, last update: 12/2/2016 (typos corrected mainly in Fig. 6, 10 and 11). pdf.