Journée pour les 60 ans d'Antonio Bucciarelli
Date : 20 juin 2023
Lieu : amphi 2A halle aux farines
Programme :
Abstracts :
- 9H30 Vincent Padovani
Starlings
- 10h00 Flavien Breuvart
Un regard nouveau sur la logique indexée
Je montrerais comment la logique indexée peut être modulée pour capturer les types intersection idempotent mais aussi plein d'autres systèmes qu'il restent à explorer. Je montrerais aussi comment on peut étendre l'idée à d'autres opérateurs logiques (exemples des monades et des points fixes de μLL). Je montrerais enfin comment, en la restreignant à des fragments spécifiques, on obtient "gratuitement" le typage intersection des lambda-calculs CbV, CbN, non typé, de types algébriques, ou encore de certains lambda-calculs infinitaires.
- 11h00 Victor Arrial et Delia Kesner
Quantitative Inhabitation
- 11h30 Giulio Manzonetto
TBA : To Bucciarelli Antonio
Some anecdotes, some collaborations, some friendship.
- 12h00 Thomas Ehrhard
My scientific life with Antonio
- 14h00 Giulio Guerrieri
The theory of meaningfulness in the call-by-value lambda-calculus
The untyped lambda-calculus is a simple and Turing-complete model of computation that represents the kernel of any functional programming language. The semantics of the untyped call-by-name lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless terms, and meaningful terms can be identified with the solvable ones. The semantics of the untyped call-by-value lambda-calculus (CbV, which is closer to the real implementations of programming languages) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory. We argue that in CbV, the correct notion of meaningful terms is captured by the concept of potential valuability. In particular, terms that are not potentially valuable provide a consistent notion of meaningless terms in CbV.
- 14h30 Christian Retoré
The sequentiality connective of pomset logic, from its denotational semantics to its proof-theoretical syntax
This talk presents old and new results on pomset logic (1993, Retoré) , a logic that extends classical commutative multiplicative linear logic with a self dual non-commutative and associative connective that we christened « before » (précède in French) before Guglielmi (1999) gave it the nickname « sequential » in his calculus of order and interaction. We start with the category of coherence spaces where there is exactly one binary multiplicative connective apart from « times » and « par ». The « before » connective enjoys intriguing properties: « before » is associative, non commutative and self-dual. We designed a proof net calculus which is complete in the sense that the syntactic correctness of a proof structure P is equivalent to the semantic correctness of the interpretation of P in the the corresponding coherence space. We show that BV (2001, Gulgliemi & Strassburger) can be viewed as a rewriting version of pomset logic (thus providing a simple proof of BV « cut elimination »). We mention that pomset calculus strictly includes BV calculus (NGuyen & Strassburger, 2022). We discuss briefly the sequent calculus for pomset logic provided by Slavnov (2020). We end the talk with a few words about a self dual modality for sequential duplication and contraction, whose semantics is well defined but which misses a proper syntax up to now.
- 15h30 Pasquale Malacaria
Axioms for Information theories
Claude Shannon revolutionized our understanding of information: He connected information with entropy, a concept originating in physics as a measure of uncertainty. Following his work several other entropy measures have been introduced with applications to several fields, from physics to cryptography. We present an axiomatization for these information theories. The axioms are based on the concept of core-concavity (a weakening of concavity having quasi-concavity as limit) and allow for a unified view of Information theories, and to general proofs of important information theoretical inequalities like Fano inequality and several others.
(Joint work with Arthur Amerigo and Arman Khouzani)
- 16h00 Nino Salibra
A journey from lambda calculus to clone algebras
Contacte : breuvart@lipn.univ-paris13.fr