[TYPES] Paper announcement: Intersection types à la Church

[Luigi Liquori INRIA]

I'm pleased to announce the available of a new paper on Intersection  
Types à la Church:

http://dx.doi.org/10.1016/j.ic.2007.03.005

http://www-sop.inria.fr/members/Luigi.Liquori/PAPERS/ic-07.pdf

As always, comments and suggestions are welcome.


Luigi Liquori and Simona Ronchi Della Rocca.


Intersection-Types à la Church

by

Luigi Liquori
INRIA Sophia Antipolis, France
Simona Ronchi Della Rocca
Dipartimento di Informatica, Università di Torino, Italy

Abstract
In this paper, we present Λt∧, a fully typed λ-calculus based on  
the intersection-type system
discipline, which is a counterpart à la Church of the type assignment  
system as invented
by Coppo and Dezani. The relationship between Λt∧ and the  
intersection type assignment
system is the standard isomorphism between typed and type assignment  
system, and so
the typed language inherits from the untyped system all the good  
properties, like subject
reduction and strong normalization. Moreover both type checking and  
type reconstruction
are decidable.

Key words: Logics and Intersection-Types, λ-calculus à la Curry and  
à la Church



-- 
  Luigi Liquori, H.d.R., Ph.D.
  INRIA Researcher, Sophia Antipolis Méditerranée
  LogNet Research Team
  Vox      : +33 4 92 38 71 93
  Fax      : +33 4 92 38 79 71
  Hom    : +33 4 93 67 09 72
  MobFr : +33 6 65 39 51 32
  MobIt   : +39 3 49 16 56 45 1
  SIP       : luigi_liquori at voip.wengo.fr
  Url        : www-sop.inria.fr/members/Luigi.Liquori
  Url        : www.inria.fr/recherche/equipes/lognet.en.html
  Email   : Let (*,#)=(.,@) in Luigi*Liquori#inria*fr
  Addr    : INRIA, 2004 Route des Lucioles - BP 93
                 FR-06902 Sophia Antipolis, France
ü
	Pensez à la planète et n'imprimez ce message que si nécessaire !
	Earth will kind ask you to print this message only if really needed!
ü