Proofs and algorithms seminar: Cristian Sottile on Monday 30 June 2025 at 15h00, "Strong normalization through idempotent intersection types: a new syntactical approach"

===== 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 Cristian Sottile (LoReL team, Instituto de Ciencias de la Computación (Universidad de Buenos Aires, CONICET)), invited by the Partout team.

***** Monday 30 June 2025 at 15h00, room Henri Poincaré *****

Cristian Sottile -- Strong normalization through idempotent intersection types: a new syntactical approach

It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems rely on semantical techniques. In this work, we study Λe∩, a variant of Coppo and Dezani's (Curry-style) intersection type system, and we propose a syntactical proof of strong normalization for it. We first design Λi∩, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in Λi∩ implies SN through a measure that, given a term, produces a natural number that decreases along with reduction. Finally, the result is extended to Λe∩, since the two systems simulate each other.

The following seminar will be on Thursday 10 July 2025 at 15h00 by Adel Bouhoula: Three Decades Advancing Automated Induction, From Test Sets to Constrained Tree Grammars and Primal Grammar Schematization.

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