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. © 2002 Published by Elsevier Science B.V.

Simple Easy Terms

ALESSI, Fabio;
2003

Abstract

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. © 2002 Published by Elsevier Science B.V.
File in questo prodotto:
File Dimensione Formato  
simple-easy.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Non pubblico
Dimensione 267.05 kB
Formato Adobe PDF
267.05 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/902556
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact