Proofs and algorithms seminar: Sam van Gool on Friday 11 April 2025 at 14h00, "Separation, duality, and profinite lambda calculus"

===== Seminar of the proofs and algorithms pole =====

Hello everybody,

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Sam van Gool (IRIF), invited by the PARTOUT team.

***** Friday 11 April 2025 at 14h00, room Grace Hopper *****

Sam van Gool -- Separation, duality, and profinite lambda calculus

Separation problems are a natural strengthening of membership problems,
and can be used to transfer decidability properties from one class to
the other. More precisely, the separation problem for a class C of
regular languages asks, given as input two regular languages A and B, to
construct a language in C that contains A and is disjoint from B, if
there exists one, and return `impossible' otherwise. In the first part
of this talk, I will illustrate this framework by discussing a solution
to separation of regular languages of countable ordinal words when C is
the class of languages definable in first-order logic [1]. This will
naturally lead to a convenient framing of separation problems in terms
of topological duality theory for distributive lattices [2], when
applied to profinite monoids and regular languages. In the second part
of this talk, I will then show how, using this theory, we recently
constructed a new profinite model of the simply typed λ-calculus [3].
This model is closely related to the theory of higher-order automata and
higher-order regular languages, leading to a number of exciting new
questions about definability and separation for such languages.

[1] T. Colcombet, S. v. Gool, R. Morvan, "First-order separation over
countable ordinals", Foundations of software science and computation
structures (FoSSaCS), 2022.

[2] M. Gehrke and S. v. Gool, Topological Duality for Distributive
Lattices: Theory and Applications, Cambridge University Press, 296pp. 2024.

[3] S. v. Gool, P.-A. Melliès and V. Moreau, Profinite lambda-terms and
parametricity, Mathematical Foundations of Programming Semantics (MFPS),
2023.


The following seminar will be on Tuesday 01 April 2025 at 10h30 by Simon Wietheger: Training One-Dimensional Graph Neural Networks is NP-Hard.

The list of upcoming seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics

To unsubscribe from this mailing list visit:
https://sympa.lix.polytechnique.fr/lists/signoff/proofs-algorithms-seminar