Speaker: Simona Ronchi della Rocca (Universidade de Turim)

Date: 4th of July 2024, 14h30

Venue:  Sala B4009 (sala de seminários do DMAT) , Departamento de Matemática (a confirmar)

Online: https://videoconf-colibri.zoom.us/j/93344876599?pwd=ejkrZ3FpYkh0NE1YV3NCdGFMOGw3QT09

Abstract. Intersection types, defined in the years ’80 of the last century by Coppo and Dezani, are a powerful tool to prove both syntactical and semantical properties of lambda-calculus. We will focus on the intersection type assignment system, characterising strongly normalisation (SN), i.e., assigning types to all and only the strongly normalising lambda terms. Such a system exists in two versions, depending on wether intersection enjoys idempotency (A^A = A) or not. While in the latter case the characterisation proof is easily carried on by induction on derivation, in the former the proof of the implication “typability implies SN” is quite difficult. The most known one is by Pottinger, through a variant of reducibility candidates, but there are also two syntactical proofs, using a decreasing measure which is a multiset (Kfoury and Wells) and a list respectively (Boudol). Both these proofs use a specific normalisation strategy. We supply a syntactical proof which is simpler than both, in the sense that its measure is a natural number and moreover it works on all reduction strategies.

Let us call extrinsically typed language the set of lambda terms that can be typed in the idempotent intersection type assignment system. We first introduce an intrinsic version of it, i.e., a typed language where types occur inside terms, so making possible to define a complete development, guided by types, which is terminating. Then we extend the language with memory to allow for counting the memories left in the normal form during the reduction: the number of such memories supplies the measure. The intrinsic and extrinsic languages simulate each-other, so the result extends naturally to the extrinsically typed language.