Simple easy terms : dart-reports : Ale+Lus:ITRS-2002

Fabio Alessi and Stefania Lusin

Simple easy terms

In Proceedings of the 2nd Workshop on Intersection Types and Related Systems, 2002 The ITRS '02 proceedings appears as vol. 70, issue 1 of Elec. Notes in Theoret. Comp. Sci., 2003-02

We illustrate the use of intersection types as a semantic tool for proving easiness result on lambda-terms. We single out the notion of em simple easiness/ for lambda-terms as a useful semantic property for building filter models with special purpose features. Relying on the notion of em easy intersection type theory, given lambda-terms M and E, with E simple easy, we successfully build a filter model which equates interpretation of M and E, hence proving that simple easiness implies easiness. We finally prove that a class of lambda-terms generated by omega₂omega₂ are simple easy, so providing alternative proof of easiness for them.

[ bib | .pdf ]

Back

This file has been generated by bibtex2html 1.43