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 Polymorphism

Authors: M. Clarence Protin ; Gilda Ferreira ORCID-iD

    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
    Fundings :
      Source : OpenAIRE Research Graph
    • LASIGE - Extreme Computing; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: UIDP/00408/2020
    • 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

    Share

    Consultation statistics

    This page has been seen 649 times.
    This article's PDF has been downloaded 323 times.