Thursday 6 October 2022, 2:00 PM, room 3U42: Strong normalisation in a System F modulo isomorphisms, Cristian Sottile (Universidad de Buenos Aires).

Two types A and B are isomorphic if there are two functions f : A => B and g : B => A such that g • f is the identity in A and f • g is the identity in B. In other words, f and g do not lose information. In the early 90's Di Cosmo et. al. characterized the complete relation of isomorphic types for the simply typed lambda calculus and several extensions, giving sets of axiomatic isomorphisms from which every existing isomorphism can be derived. In 2012 Díaz-Caro and Dowek introduced System I, an extension to the simply typed lambda calculus where isomorphic types are equated by a congruence relation based on the axiomatic isomorphisms given by Di Cosmo. The aim of this system is to take advantage of the fact that two corresponding programs p : A and p' : B can be transformed into each other when A and B are isomorphic (i.e. f(p) = p' and g(p') = p), by allowing to use p' where p is expected, without the need of applying the explicit conversion.

In this talk I will present Polymorphic System I, a polymorphic extension where we added the type isomorphisms related to the universal quantifier. In particular, I will discuss a work-in-progress technique we are developing to prove strong normalisation, which extends that of System I non-trivially.