D. Barbarossa :: Research

Research Activity of Davide Barbarossa

Depuis les Grecs qui dit mathématique dit démonstration.
-- Nicolas Bourbaki (Éléments de mathématique; Théorie des ensembles).

Academic Interests

I study computation from a mathematical point of view, and mathematics from a computational one.
In particular, I do research at the intersection between programming language theory and mathematical logic.

More specifically, I am usually thinking about the following topics:

λ-calculi (especially via Program Differentiation, Category Theory and Operational Semantics)
Logic from a Computational POV (especially Proof Theory via Curry-Howard, Linear Logic and Realisability/Dialectica)
Formal Methods for Functional Programming (especially via Semantics and Type Theories).

If you have no clue about what all this is about, this might help you.

I am also interested in the philosophy of mathematics, for which I would like to reconsider a transcendental approach (in a renewed sense of Kant's).
I am also interested in the philosophy of physics and of science in general.

Currently, the following thoughts fill my mind...

Differential λ-calculus and geometry for Automatic Differentiation

Tropical mathematics for λ-calculi

Dialectica from an imperative point of view

Responsabilities

Co-organiser of the International Workshop on Programs from Proofs, Bath, UK, 2025
Program Committee member of the 9th International Workshop on Trends in Linear Logic and Applications (TLLA), Birmingham, UK, 2025
Co-organiser of the international workshop Directions and perspectives in the λ-calculus, Bologna, Italy, 2024
Member of AILA (Associazione Italiana per la Logica e le sue Applicazioni), and of GT Scalp (Structures formelles pour le CALcul et les Preuves)
Reviewer for: international conferences and journals -- LICS, FSCD, CSL, FoSSaCS, MFPS, LMCS, MSCS, ToCL; for books -- Chapter 2 and Chapter 8 of: A Lambda Calculus Satellite (by H. Barendregt and G. Manzonetto).

Papers

Preprints (submitted or work in progress)
- 2025: An excursion into Dialectica and Differentiation (arxiv)
Published (with peer review)
- On the algorithmic structure of Dialectica realisers (slides) (PDF) (extended version: arxiv)
  Davide Barbarossa and Thomas Powell
  Proceedings of the 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)
- Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages (slides) (PDF) (extended version: arxiv)
  Davide Barbarossa and Paolo Pistone
  Proceedings of the ACM on Programming Languages, Volume 10 (POPL 2026)
- Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs (PDF) (extended version: arxiv)
  Davide Barbarossa and Paolo Pistone
  Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
- Resource approximation for the λμ-calculus (slides) (PDF) (extended version: see my PhD thesis)
  Davide Barbarossa
  Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)
- Taylor Subsumes Scott, Berry, Kahn and Plotkin (PDF) (extended version: see my PhD thesis)
  Davide Barbarossa and Giulio Manzonetto
  Proceedings of the ACM on Programming Languages, Volume 4 (POPL 2020)
  The paper received a Distinguished Paper Award from the POPL program committee!

Invited Lectures and Talks at International and National Academic Events

2026, Rencontres mensuelles ``CHoCoLa'' (ENS-Lyon, France)
Seminar: Computational interpretations of logic : the case of Dialectica (slides)
2025, Workshop ``Realizability'' (CIRM, France)
Seminar: Dialectica, its realisers and Hoare logic (slides)
2024, 8th International Workshop on Trends in Linear Logic and Applications ``TLLA'' (Tallinn, Estonia)
Tutorial: Differential aspects of the approximation theory of the lambda-calculus (on blackboard)

Abstract

In this tutorial, we will study the notion of approximation for the lambda-calculus. After having introduced the topic, we will focus on the so-called "resource approximation" and use it in order to prove the Continuity Lemma for the lambda-calculus. We will then see how this approximation technique is actually related to the notion of differentiation in the lambda-calculus on the one hand, and how it provides an abstraction of the usual notion of differentiation from mathematical analysis on the other hand, by looking (time permitting) at its categorical formulation.
2024, 5th Southen Midlands Logic Seminar (Bath, UK)
Seminar: An overview of (Tropical) Quantitative Semantics and Taylor Expansion for the λ-calculus (slides)
2023, Journée d'ètude ``Logique, langage et computation'' : autour de la logique linéaire et ses interfaces (Lyon, France)
Seminar: Réflexions sur les fondements des mathématiques, à la lumière de l'informatique (transparents).

Workshops, Congress Communications (with peer review)

2024, Tallinn (Estonia), 8th International Workshop on Trends in Linear Logic and Applications (TLLA): Stability property for the Call-by-Value λ-calculus through Taylor expansion (slides) (pdf)
2023, Palermo (Italy), 24th Italian Conference on Theoretical Computer Science (ICTCS): Tropical Mathematics and the λ-calculus (slides) (pdf)

2023, Roma (Italy), 7th International Workshop on Trends in Linear Logic and Applications (TLLA): Tropical Mathematics and Linearity in λ-calculus (slides)
2022, Caserta (Italy), XXVII Incontro of Associazione Italiana di Logica e sue Applicazioni (AILA): An overview on the Taylor expansion of programs (slides)
2022, Haïfa (Israel), Joint 7th International Workshop on Linearity and 6th International Workshop on Trends in Linear Logic and Applications (TLLA): Denotational semantics driven simplicial homology? (slides) (pdf)
2019, Pavia (Italy), XXI Congresso Unione Matematica Italiana: Introduzione alla Realizzabilità classica di Krivine (lucidi)
2019, Dortmund (Germany), 3rd International Workshop on Trends in Linear Logic and Applications (TLLA): On the power of Taylor Expansion.

Research Seminars

2026, Université Aix-Marseille (France), Laboratoire d'Informatique et des Systèmes (LIS): Tropical Geometry of Probabilistic Programming Languages

2026, Université Paris Est - Créteil (France), Laboratoire d'Algorithmique, Complexité et Logique (LACL): Computational interpretations of logic : the case of Dialectica and Realisability. (slides)

2025, Università Roma Tre (Italy), Workshop ``Trends in Proof-Theory of Linear Logic'': Are critical foundations of mathematics possible?

2025, University of Bath (UK), Workshop ``Programs from Proofs'': Dialectica and Hoare Logic

2025, Università Roma Tre (Italy), Kickoff meeting of the International Research Network ``Logic and Interaction'': On the tropical geometry of probabilistic programming languages

2024, Università Roma Tre (Italy), Workshop ``Trends in Proof-Theory of Linear Logic'': An overview on Dialectica as Differentiation (slides)

2024, University of Sussex (UK), School of Informatics: An overview on Dialectica and Differentiation

2024, Swansea University (UK), Department of Computer Science: Informal lecture on the differential λ-calculus

2024, Université Paris Est - Créteil (France), Laboratoire d'Algorithmique, Complexité et Logique (LACL): Lambda-Calculus, Taylor Expansion and (Tropical) Quantitative Semantics: an overview

2023, CIRM, France, Journées d'hiver du GT Scalp: λ-calculus goes to the tropics

2023, Université Savoie Mont Blanc (France), Laboratoire de Mathématiques (LAMA): λ-calculus goes to the tropics

2022, Université Paris Cité (France), Institut de Recherche en Informatique Fondamentale (IRIF): λ-calculus goes to the tropics (on blackboard)

2021, ENS de Lyon (France) (Video Conference due to Covid19), Laboratoire de l'Informatique du Parallélismse (LIP): Le λμ-calcul avec ressources, et des applications (slides_english)

2020, Università di Bologna (Italy) (Video Conference due to Covid19), Dipartmento di Informatica (DIAPASoN group): The resource λμ-calculus, and applications

2020, University of Bath (UK) (Video Conference due to Covid19), Department of Computer Science: Approximating functional programs: Taylor subsumes Scott, Berry, Kahn and Plotkin (slides)

2020, Université Savoie Mont Blanc (France), Laboratoire de Mathématiques (LAMA): Approximations partielles et approximation par ressources en λ-calcul (on blackboard)

2018, Università Roma Tre (Italy), Dipartimento di Matematica e Fisica: Realizzabilità classica ed ultrafiltri su N (lucidi).

Reports (with peer review)

PhD: Towards a resource based approximation theory of programs..
There is an Errata Corrige: it's about small details, but especially if you are reading Section 3.5 you would want to have a look at it.
You can also look at the slides of the defence.
Main topics: λ-calculus, λμ-calculus, Taylor expansion and resources approximation.
Master: On the computational content of proofs.
This is the English version for the Italian defence, which contains the content of the French version (as Chapter 3).
You can also look at the slides of the defence (in their French version for the French defence).
Main topics: Curry-Howard correspondence, Krivine's classical realisability.

Notes (no peer review)

2025: Lecture notes for a one week course I gave at the ESSLLI25 summer school. You can also find the slides at the link.
2022: λ-calculus is not an exotic mathematical subject (pdf)