M. Clarence Protin ; Gilda Ferreira - Typability and Type Inference in Atomic Polymorphism

lmcs:7417 - Logical Methods in Computer Science, August 12, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:22)2022
Typability and Type Inference in Atomic PolymorphismArticle

Authors: M. Clarence Protin ORCID; Gilda Ferreira ORCID

    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.


    Volume: Volume 18, Issue 3
    Published on: August 12, 2022
    Accepted on: July 6, 2022
    Submitted on: April 29, 2021
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03B15, 03B20, 03B40, 03B70, 03F03,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • LASIGE - Extreme Computing; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: UIDB/00408/2020
    • Center for Mathematics, Fundamental Applications and Operations Research; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: UIDB/04561/2020
    • LASIGE - Extreme Computing; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: UIDP/00408/2020

    Consultation statistics

    This page has been seen 1514 times.
    This article's PDF has been downloaded 424 times.