View Related Documents

Abstract

We consider a version of the Mitchell's polymorphic type containment (aka subsumption). Here, it is not suited for the system F but for the predicative version of it introduced by Leivant. The aim of the approach is to propose a new notion of polymorphic functional subsumption which may be decidable unlike Mitchell's one. We define a system for predicative subsumption in the style of Mitchell and then prove its equivalence with a Gentzen-style definition. Next, we study the notion of bicoercibility. This is followed by a reduction of the typability in the Leivant's system with subsumption to subsumption itself.

Fulltext Preview

Image of the first page of the fulltext document