Principal Typing in a ∀Λ-Discipline

Publisher Website
Google Scholar
Abstract
In this paper we study the problem of finding a principal typing for a λ-term in a polymorphic intersection type assignment system. Following the approach of Coppo et al., Ronchi and Venneri, the principal type is proved to exist for any λ-term with a finite set of approximants. In the same way the existence of the principal type is shown for BCKλ-terms in a polymorphic type assignment system.

This publication has 0 references indexed in Scilit: