Research Activity of Davide Barbarossa
La mathématique est l'art de donner le même nom à des choses différentes.
-- Henri Poincaré (Science et méthode).
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 languages theory and mathematical logic.
More specifically, I am usually working within the following Curry-Howard-Lambek'ish topics:
λ-calculus
Linear Logic
Category theory
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 currently mainly wondering about...
Tropical models of differential λ-calculus
What is an approximation of a programming language?
Denotational semantics driven simplicial homology
Responsabilities
- Co-organiser of the workshop Directions and perspectives in the λ-calculus, Bologna, 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 and ``sub-reviewer'' for international conferences and journals: LICS, LMCS, FSCD, FoSSaCS, MFPS, CSL.
- Reviewer for books: Chapter 2 and Chapter 8 of: A Lambda Calculus Satellite (by H. Barendregt and G. Manzonetto).
Conference and Journal papers (with peer review)
- Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs (long version)
Davide Barbarossa and Paolo Pistone
Accepted to appear on CSL 2024
- Resource approximation for the λμ-calculus (pdf) (bib) (slides) (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) (bib) (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!
Workshops, Congress Communications (with peer review)
2023, Palermo (Italy), 24th Italian Conference on Theoretical Computer Science (ICTCS):
Tropical Mathematics and the λ-calculus (slides) (long abstract)
2023, Roma (Italy), 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), Trends in Linear Logic and Applications (TLLA):
Denotational semantics driven simplicial homology? (slides) (long abstract)
2019, Pavia (Italy), XXI Congresso Unione Matematica Italiana:
Introduzione alla Realizzabilità classica di Krivine (slides - italian)
2019, Dortmund (Germany), Trends in Linear Logic and Applications (TLLA):
On the power of Taylor Expansion.
Reports (with peer review)
Drafts (no peer review)
λ-calculus is not an exotic mathematical subject (pdf)
Seminars
2023, Journée interdisciplinaire ``Logique, Langage et Computation'' (Lyon, France): Réflexions sur les fondements des mathématiques, à la lumière de l'informatique (transparents)
2023, Université Savoie Mont Blanc (France), Laboratoire de Mathématiques (LAMA): λ-calculus goes to the tropics
2023, Journées d'hiver du GT Scalp (CIRM, France): λ-calculus goes to the tropics (slides)
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 (slides_italian).
Other attended events
2022, Paris (France), Workshop in honour of Thomas Ehrhard's 60 birthday, at "CNAM"
2022, Online (the web), Workshop Proof, Computation and Meaning
2022, Marcoux (France), École thématique "Computation et algorithmes : anciens et nouveaux enjeux pour la philosophie des mathématiques", at Château de Goutelas
2022, Marseille (France), Mois thématique "Logique et Interactions" (week 1: école d'hiver de logique linéaire, week 2: Logique de la programmation probabiliste; week 3: Logique et transdisciplinarité) at "CIRM"
2021, Fontainebleau (France), Journées Scalp
2020 Covid19 pandemic, in lockdown (home), Several video conferences
2019, Rome (Italy), General Meeting of the IRN Linear Logic and Conference in honour of Michele Abrusci's Retirement Day
2019, Paris (France): Research school in computational complexity at "Institut Henri Poincaré"
2019, Île de Porquerolles (France): Summer School on Topology, Algebra, and Categories in Logic
2018, Paris (France): GDRI Linear Logic Plenary Meeting
2018, Marseille (France): Journées LHC - Logique, homotopie, catégories
2018, Marseille (France): Realizability workshop at "Centre International de Rencontres Mathématiques"
2017, Rome (Italy): General meeting of the GDRI Linear Logic and Conference in honour of Jean-Yves Girard's 70th birthday
2016, Lyon (France): International meeting on Linear Logic: interaction, proofs and computation.
Page maintained by Davide Barbarossa