Towards an Intersection Typed System à la Church
Résumé
In this paper, we presents a comfortable fully typed lambda calculus based on the well-known intersection type system discipline where proof are not only feasible but easy; the present system is the counterpart à la Church of the type assignment system as invented by Coppo and Dezani.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...