Accessibility setting

Section: New Results

Intersection types

Participants : Alexis Bernadet [Contact] , Stéphane Lengrand [(CNRS, Lix)] .

Alexis Bernadet and Stéphane Lengrand have studied a typing system for the $\lambda$-calculus with non-idempotent intersection types. As it is the case in (some) systems with idempotent intersections, a $\lambda$-term is typable if and only if it is strongly normalizing. Non-idempotency brings some further information into typing trees, such as a bound on the longest β-reduction sequence reducing a term to its normal form. These results are presented in Klop’s extension of $\lambda$-calculus, where the bound that is read in the typing tree of a term is refined into an exact measure of the longest reduction sequence. This complexity result is, for longest reduction sequences, the counterpart of de Carvalho’s result for linear head-reduction sequences. This work is described in a paper published in the prooceedings of the FOSSACS 2011 conference [22] .

Alexis Bernadet and Stéphane Lengrand have also revisited models of typed $\lambda$-calculus based on filters of intersection types. By using non-idempotent intersections, they simplify a methodology that produces modular proofs of strong normalization based on filter models. Non-idempotent intersections provide a decreasing measure proving a key termination property, simpler than the reducibility techniques used with idempotent intersections. Such filter models are shown to be captured by orthogonality techniques: we formalize an abstract notion of orthogonality model inspired by classical realizability, and express a filter model as one of its instances, along with two term-models (one of which captures a now common technique for strong normalization). Applying the above range of model constructions to Curry-style System F describes at different levels of detail how the infinite polymorphism of System F can systematically be reduced to the finite polymorphism of intersection types. This work is described in a paper published in the prooceedings of the CSL 2011 conference [23] .