Rencontre, March 10, 2022
Programme
 10:30 – 12:00

Denis Kuperberg (CNRS  LIP)Invited talk: Positive Firstorder Logic on Words and Graphs
[The talk will take place in room M7 411, 4th floor, turn left when you exit the elevator.]
We will investigate the gap between syntactically and semantically positive firstorder logic formulas.
A formula is syntactically positive if it does not contain negated predicates, while it is semantically positive when the class of structures it defines is monotone, i.e. closed under making the predicates true on more tuples.
Starting with finite words, I will present the logic FO+, where letter predicates are required to appear positively. The words considered here are on a "powerset alphabet": predicates a(x) and b(x) can be true simultaneously on the same position x of the word. We will ask a syntax versus semantics question: FO+definable languages are monotone in the letters, but can every FOdefinable monotone language be expressed in FO+ ? On general structures, Lyndon's theorem gives a positive answer to this question, but it is known to fail on finite structures. We will see that it already fails on finite words, by giving a simple counterexample language. This gives a new proof for the failure of Lyndon's theorem on finite structures, that is much more elementary than previous proofs.
We will also study the problem on finite graphs: if a class of finite graphs is FOdefinable and closed under edge addition, can it be defined with a negationfree formula ? To our knowledge this was an open question, which we can answer negatively via a suitable encoding of our counterexample language.
Finally, if time permits, we will go back to regular languages of finite words and see that FO+definability is surprisingly undecidable in this framework.
This talk is based on work published in LICS 2021, with a full version currently submitted to a special issue of LMCS, available on Arxiv.
 14:00 – 15:00

Loïc Pujet (Gallinette, INRIA)Invited talk: Extensionality in intensional type theory
[The talk will take place in amphi A, 3rd & 4th floors, at the other end of the corridor w.r.t. amphi B, if you know where this is.]
MartinLöf Type Theory is a sweet spot in the correspondence between proofs and programs: dependent types and inductive types allow for remarkably expressive program specifications, and adding a universe hierarchy results in a theory with enough logical power to encode most daytoday mathematical constructions  an allaround foundational tool for proof assistants.
However the inductive equality supplied by MLTT is not quite suitable for mathematical reasoning, because it encodes program equality ("intensionality") instead of behavioral equality ("extensionality"). This has unfortunate consequences: one cannot prove that the functions n > n+2 and n > 2+n are equal, there is no way to quotient a type by an equivalence relation, etc.
Observational Type Theory was designed to remediate to this very state of affairs. A complete implementation of OTT would feature these desired extensionality principles, while preserving the philosophy of the correspondence between proofs and programs and the nice properties that come with it (normalization, canonicity, decidability of typing...).
In my talk, after some preliminary exposition about dependent types, I will introduce TT^obs, a conceptually simple extension of MartinLöf Type Theory that turns it into a fully observational type theory. I will illustrate with some use cases, and if time allows I will go over its metatheory.
 15:30 – 16:30

Marie Kerjean (CNRS  LIPN)Invited talk: ∂ is for Dialectica
[The talk will take place in amphi A, 3rd & 4th floors, at the other end of the corridor w.r.t. amphi B, if you know where this is.]
Dialectica is a proof transformation acting of intuitionnistic logic which factors through Girard's translation, allowing the realization of several semiclassical axioms such as Markov's principle. By taking the viewpoint of differential lambdacalculus and recent developments in differentiable programming, we will show how Dialectica computes higherorder backward differentiation. We will illustrate this through the lens of categories, types and lambdaterms.
This is joint work with PierreMarie Pédrot.