Research Activity of Davide Barbarossa
Les mathématiciens n'étudient pas des objets, mais des relations entre les objets ;
-- Henri Poincaré (La Science et l'Hypothèse).
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 working within the following Curry-Howard-Lambek'ish topics:
λ-calculus and in general functional programming
Linear Logic and in general proof theory
Category theory and in general semantics of programming languages
Type Theories and in general verification of programs.
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).
Currently, the following thoughts fill my mind...
Dialectica transformation, Hoare Logic, differential geometry/λ-calculus
Tropical mathematics for λ-calculi
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, LMCS, FSCD, FoSSaCS, MFPS, CSL; 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: On the algorithmic structure of Dialectica programs (arxiv)
- 2025: Tropical Geometry of Probabilistic Programming Languages (arxiv)
- 2025: An excursion into Dialectica and Differentiation (arxiv)
- Published (with peer review)
- Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs (PDF) (long version: arxiv)
Davide Barbarossa and Paolo Pistone
32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
- Resource approximation for the λμ-calculus (slides) (PDF) (long version: see my PhD thesis)
Davide Barbarossa
36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022)
- Taylor Subsumes Scott, Berry, Kahn and Plotkin (PDF) (long version: see my PhD thesis)
Davide Barbarossa and Giulio Manzonetto
Principles of Programming Languages (POPL) 2020, PACMPL Vol. 4, pp. 1:1-1:23
The paper received a Distinguished Paper Award from the POPL program committee!
Invited Lectures and Talks at International and National Academic Events
- 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)
- 2025, Roma (Italy), International Research Network ``Logic and Interaction'' -- Kickoff meeting:
On the tropical geometry of probabilistic programming languages
(slides)
- 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)
- 2023, Journées d'hiver du GT Scalp (CIRM, France):
λ-calculus goes to the tropics
- 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
- 2025, University of Bath (UK), Workshop ``Programs from Proofs'': Dialectica and Hoare Logic (slides)
- 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, Université Paris Est - Créteil (France), Laboratoire d'Algorithmique, Complexité et Logique (LACL): Lambda-Calculus, Taylor Expansion and (Tropical) Quantitative Semantics: an overview
- 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)
- 2022: λ-calculus is not an exotic mathematical subject (pdf)
Page maintained by Davide Barbarossa