Typability and Type Inference in Atomic Polymorphism
From MaRDI portal
Publication:6366343
arXiv2104.13675MaRDI QIDQ6366343FDOQ6366343
Authors: M. Clarence Protin, Gilda Ferreira 
Publication date: 28 April 2021
Abstract: It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in Curry style variants of system Fat and show that typability is decidable and that there is an algorithm for type inference which is capable of dealing with non-redundancy constraints.
This page was built for publication: Typability and Type Inference in Atomic Polymorphism
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6366343)
