$ Thomas Ehrhard: page personnelle
IRIF

Thomas Ehrhard

Dernière mise à jour : 17/03/2024

IRIF
Université Paris Cité
Bâtiment Sophie Germain, Case courrier 7014
75205 PARIS Cedex 13

Tél : +33-1 57 27 92 17

Bureau 4014a.

ehrhard@irif.fr

Thomas Ehrhard

Généralités

I am a CNRS senior researcher.

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.

Teaching

Some documents (recent publication list, see also DBLP).

Thomas Ehrhard. A categorical semantics of constructions. Logic in Computer Science. Third Symposium on Logic in Computer Science, Edinburgh, 1988. IEEE. 1988. pdf.

Thomas Ehrhard. Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science, Cambridge University Press. 1993. pdf.

Loïc Colson, Thomas Ehrhard. On strong stability and higher-order sequentiality. Logic in Computer Science. Ninth Symposium on Logic in Computer Science, Paris, 1994. IEEE. 1994. pdf.

Antonio Bucciarelli, Thomas Ehrhard. Sequentiality in an extensional framework. Information and Computation, Academic Press. 1994. pdf.

Thomas Ehrhard. Projecting sequential algorithms on strongly stable functions. Annals of Pure and Applied Logic, North Holland. 1996. pdf.

Nuno Barreiro, Thomas Ehrhard. Anatomy of an extensional collapse. 1997. Unpublished manuscript. pdf.

Thomas Ehrhard. A relative definability result for strongly stable functions and some corollaries. Information and Computation, Academic Press. 1999. pdf.

Thomas Ehrhard. Parallel and serial hypercoherences. Theoretical Computer Science, Elsevier. 2000. pdf.

Antonio Bucciarelli, Thomas Ehrhard. On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic, North Holland. 2000. pdf.

Antonio Bucciarelli, Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, North Holland. 2001. pdf.

Thomas Ehrhard. On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, Cambridge University Press. 2002. pdf.

Thomas Ehrhard. A completeness theorem for symmetric product phase spaces. Journal of Symbolic Logic, Association for Symbolic Logic. 2004. pdf.

Thomas Ehrhard, Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, Elsevier. 2004. pdf.

Thomas Ehrhard. Web based models of linear logic. Slides of my talk at WoLLIC'04, Fontainebleau. 2004. pdf.

Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, Cambridge University Press. 2005. pdf.

Thomas Ehrhard, Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, Elsevier. 2006. To appear. pdf.

Thomas Ehrhard, Laurent Regnier. Differential interaction nets. Theoretical Computer Science, Elsevier. 2006. To appear. pdf.

Thomas Ehrhard, Laurent Regnier. 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.

Thomas Ehrhard, Laurent Regnier. Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms. 2006. Long version. pdf.

Thomas Ehrhard, Olivier Laurent. Embedding the pi-calculus in differential interaction nets. Slides of my talk at the conference Computability in Europe 2006 (CiE 2006), Swansea. 2006. pdf.

Thomas Ehrhard, Olivier Laurent. Embedding the Finitary Pi-calculus in Differential Interaction Nets. 2006. Electronically published proceedings. Available here.

Thomas Ehrhard, Olivier Laurent. On differential interaction nets and the pi-calculus. 2006. HAL technical report ccsd-00096280, version 1. Available here.

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

Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto. Not enough points is enough. 2007. Computer Science Logic. pdf.

Thomas Ehrhard, Olivier Laurent. Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. 2007. CONCUR, conference short version. pdf.

Thomas Ehrhard. Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. 2007. Slides of a talk given at University Roma III, the 16th of April. pdf.

Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto. A relational model of a parallel and non-deterministic lambda-calculus. 2008. Accepted at LFCS 09. .

Vincent Danos, Thomas Ehrhard. On probabilistic coherence spaces. 2008. PPS and CHOCO technical report. To appear in Information and Computation. pdf.

Thomas Ehrhard, Olivier Laurent. Acyclic Solos and Differential Interaction Nets. 2008. PPS and CHOCO technical report. Paru dans Logical Methods in Computer Science 6(3), 2010. pdf.

Thomas Ehrhard. The Scott model of Linear Logic is the extensional collapse of its relational model. 2009. Theoretical Computer Science 424: 20-45 (2012). pdf.

Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto. 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.

Alberto Carraro, Thomas Ehrhard, Antonino Salibra. Resource Combinatory Algebras. 2010. MFCS 2010. pdf.

Thomas Ehrhard. A Finiteness Structure on Resource Terms. 2010. LICS 2010. pdf.

Alberto Carraro, Thomas Ehrhard, Antonino Salibra. Exponentials with Infinite Multiplicities. 2010. CSL 2010 (long version, with proofs in an appendix). pdf.

Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto. Categorical Models for Simply Typed Resource Lambda-Calculus. 2010. MFPS 2010. pdf.

Thomas Ehrhard, Olivier Laurent. Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. Information and Computation, Elsevier. 2010. 208(6), pp. 606-633. pdf.

Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. 2011. Accepted at CSL 2011, Bergen. pdf.

Richard Blute, Thomas Ehrhard, Christine Tasson. A Convenient Differential Category. Cahier de Topologie et Géométrie Différentielle Catégoriques, . 2011. To appear. pdf.

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

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

Thomas Ehrhard, Michele Pagani, Christine Tasson. The Computational Meaning of Probabilistic Coherence Spaces. 2011. Accepted at LICS 2011. pdf.

Thomas Ehrhard. About the extensional collapse of Rel. 2012. Slides of a talk given at LI 2012 (CIRM, Marseille). pdf.

Thomas Ehrhard. An application of the extensional collapse of the relational model of linear logic. 2012. Submitted. pdf.

Thomas Ehrhard, Ying Jiang. CCS for trees. 2013. Submitted for publication. pdf.

Thomas Ehrhard, Ying Jiang. CCS for trees. 2013. Slides of a talk given at the workshop LOCALI 2013 (Beijing). pdf.

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

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

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

Thomas Ehrhard. Call-By-Push-Value from a Linear Logic point of view. 2015. Accepted at ESOP 2016 (long version, with proofs). pdf.

Thomas Ehrhard, Michele Pagani, Christine Tasson. Full abstraction for probabilistic PCF. 2015. Submitted for publication. pdf.

Shahin Amini, Thomas Ehrhard. On Classical PCF, Linear Logic and the MIX rule. 2015. CSL 2015, Berlin. pdf.

Thomas Ehrhard, Ying Jiang. A dendroidal process calculus. 2015. Submitted for publication. pdf.

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

Thomas Ehrhard. Call-By-Push-Value from a Linear Logic point of view. 2016. Accepted at ESOP 2016. pdf.

Thomas Ehrhard, Michele Pagani, Christine Tasson. Measurable Cones and Stable, Measurable Functions. 2017. POPL 2018. arXiv.

Thomas Ehrhard, Christine Tasson. Probabilistic Call By Push Value. 2018. To appear in LMCS. Full abstraction for a rich functional probabilistic language with general recursion and recursive types. pdf.

Thomas Ehrhard. La sémantique, un point de vue mathématique sur les programmes. 2018. Exposé donné lors de la journée scientifique à la mémoire de Maurice Nivat, le 6/2/2018. pdf.

Thomas Ehrhard. Stable and measurable functions on positive cones. 2018. Talk given at the Chocola Seminar on 8/2/2018. Joint work with Michele Pagani and Christine Tasson. pdf.

Thomas Ehrhard. Differentials and distances in probabilistic coherence spaces. 2019. Accepted at FSCD 2019. Current version: april 2019.. pdf.

Thomas Ehrhard. Derivatives and distances in probabilistic coherence spaces. 2019. Slides of a talk at PIHOC 2019. pdf.

Thomas Ehrhard. On the linear structure of cones. 2020. Published in LICS 2020. pdf.

Thomas Ehrhard. Upper approximating probabilities of convergence in probabilistic coherence spaces. 2020. IRIF research report. arXiv.

Thomas Ehrhard, Farzad Jafarrahmani. Categorical models of Linear Logic with fixed points of formulas. 2021. LICS 2021. HAL.

Thomas Ehrhard. Differentials and distances in probabilistic coherence spaces. 2021. Extended version of my FSCD 2019 paper, submitted for publication in a journal. HAL.

Thomas Ehrhard. What is Linear Logic?. 2021. A short and subjective intoduction to Linear Logic. pdf.

Thomas Ehrhard. Coherent differentiation. 2021. Differentiation of lambda-terms is compatible with determinism. Submitted for publication. pdf.

Thomas Ehrhard. Coherent differentiation. 2021. Slides of a series of talks given in the IRIF Semantics Working Group, providing an overview of the paper. pdf.

Thomas Ehrhard. A coherent differential PCF. 2022. A differential extension of PCF based on coherent differentiation. Published in LMCS. arXiv.

Thomas Ehrhard. Comparing Coherent Differentiation (CD) and AD. 2022. Slides for a talk given at the Workshop on Differentiable Programming --- Université Paris Cité, 29 and 30 June 2022. pdf.

Thomas Ehrhard, Guillaume Geoffroy. Integration in cones. 2023. IRIF technical report, last update: 14/03/2024. Submitted for publication. arXiv.

Thomas Ehrhard. Integration in Positive Cones. 2023. Slides of a talk given at the 4th ANR PPS General Meeting, 4-6 Jan 2023. pdf.

Thomas Ehrhard, Aymeric Walch. Cartesian Coherent Differential Categories. 2023. Preprint available on HAL and ArXiv, published in LICS 2023. pdf.

Thomas Ehrhard, Aymeric Walch. Coherent Taylor expansion as a bimonad. 2023. IRIF preprint, submitted for publication, last update 2/10/2023. arXiv.

Thomas Ehrhard. From Differential Linear Logic LL to Coherent Differentiation. 2024. Preprint. arXiv.

Thomas Ehrhard. Integration in cones. 2024. Slides of a talk at the seminar Chocola, ENS Lyon, 3/14/2024. pdf.