E-viri
PDF
Odprti dostop
-
Alessi, F.; Lusin, S.
Electronic notes in theoretical computer science, February 2003, 2003-02-00, Letnik: 70, Številka: 1Journal Article
We illustrate the use of intersection types as a semantic tool for proving easiness result on λ-terms. We single out the notion of simple easiness for λ-terms as a useful semantic property for building filter models with special purpose features. Relying on the notion of easy intersection type theory, given λ-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 λ-terms generated by ω2ω2 are simple easy, so providing alternative proof of easiness for them.
