The notion of type isomorphisms defines an equivalence relation upon
the types of a programming language, that has practical interest for
example for finding functions in libraries. I will speak about the
problem of axiomatisation of these isomorphisms in the case of the
lambda-calculus with product and sum types. I will show you how this
issue leads us to the problem of normalisation of this calculus, and
how we could solve it by creating a new normalisation tool, based on
partial evaluation techniques.
Most of the work I will present has been done in collaboration with
Marcelo Fiore and Roberto Di Cosmo.
|