Rencontre, 24 novembre 2022

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, Aix-Marseille Université)

Invited talk: The theory of call-by-value solvability

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 term. The semantics of the untyped call-by-value lambda-calculus (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 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.

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 first-order 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 second-order 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 excluded-middle, 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.