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

More specifically, I am usually working within the following Curry-Howard-Lambek'ish topics:

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

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 (PDF) (long version: soon on arxiv)
  Davide Barbarossa and Paolo Pistone
  32nd EACSL Annual Conference on Computer Science Logic (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!

Invited Lectures and Talks at International and National Academic Events

• 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 interdisciplinaire ``Logique, Langage et Computation'' (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) (long abstract)
  
  
• 2023, Palermo (Italy), 24th Italian Conference on Theoretical Computer Science (ICTCS): Tropical Mathematics and the λ-calculus (slides) (long abstract)
  
  
• 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) (long abstract) (bib)
  
  
• 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.
  
  

Invited Research Seminars

• 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. (bib).
  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.
  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.

Drafts (no peer review)

• λ-calculus is not an exotic mathematical subject (pdf) (bib)
  
  
• On Dialectica and Differentiation, via Categories (pdf)
  
  

Page maintained by Davide Barbarossa