Rencontre, Nov. 24, 2022
Cette rencontre se tiendra à Paris. plus précisément à l'amphithéâtre PierreGilles de Gennes au rezdechaussée du bâtiment Condorcet, sur le campus des Grands Moulins, non loin de Sophie Germain, arrêt Bibliothèque F. Mitterrand (métro 14 ou RER C).
https://www.openstreetmap.org/way/62377969
Un accueil sera proposé à partir de 10h.
Programme
 10:00 – 10:30
 accueil
 10:30 – 11:30

Daniela Petrisan (IRIF)Invited talk: Semialgebras and Weak Distributive Laws
 13:30 – 14:30

Giulio Guerrieri (LIS, AixMarseille Université)Invited talk: The theory of callbyvalue solvability
The semantics of the untyped (callbyname) lambdacalculus 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 term. The semantics of the untyped callbyvalue lambdacalculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in callbyname. 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 callbyname, 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.
This is joint work with Beniamino Accattoli, published at ICFP 2022 https://dl.acm.org/doi/10.1145/3547652
 15:00 – 16:30

Hugo Herbelin (INRIA)Invited talk: Computing with Gödel’s completeness theorem: Weak Fan Theorem, Markov’s Principle and Double Negation Shift in action
Completeness of firstorder logic against Tarski semantics, that is Gödel's completeness theorem, has been abundantly studied in the context of classical and intuitionistic reverse mathematics in either secondorder arithmetic or set theory, sometimes with inconsistent results (e.g. Krivine asserting it is fully constructive, Kreisel deriving Markov's principle, McCarty asserting it requires excludedmiddle, Simpson asserting it is classically Weak Kőnig Lemma, Henkin that it is classically the Ultrafilter Theorem, etc.).
We will survey these results, sorting out the reasons for these apparently inconsistent results, eventually clarifying that completeness with respect to Tarski semantics over recursively enumerable theories intuitionistically requires:
 a purely intuitionistic (unexpected) predicative form of the Weak Fan Theorem for dealing with the underlying logical structure and the negative connectives,
 Markov's Principle for dealing with positive/additive falsity,
 a form of Double Negation Shift for dealing with positive disjunction.
Interestingly, Markov's Principle and Double Negation Shift are weakly classical principles which preserve the witness and disjunction properties, and thus, are in this sense "valid" intuitionistic principles.