{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:09Z","timestamp":1753894389685,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T00:00:00Z","timestamp":1660262400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P.","award":["UIDP\/00408\/2020"],"award-info":[{"award-number":["UIDP\/00408\/2020"]}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P.","award":["UIDB\/00408\/2020"],"award-info":[{"award-number":["UIDB\/00408\/2020"]}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P.","award":["UIDB\/04561\/2020"],"award-info":[{"award-number":["UIDB\/04561\/2020"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>It is well-known that typability, type inhabitation and type inference are\nundecidable in the Girard-Reynolds polymorphic system F. It has recently been\nproven that type inhabitation remains undecidable even in the predicative\nfragment of system F in which all universal instantiations have an atomic\nwitness (system Fat). In this paper we analyze typability and type inference in\nCurry style variants of system Fat and show that typability is decidable and\nthat there is an algorithm for type inference which is capable of dealing with\nnon-redundancy constraints.<\/jats:p>","DOI":"10.46298\/lmcs-18(3:22)2022","type":"journal-article","created":{"date-parts":[[2022,8,17]],"date-time":"2022-08-17T07:31:51Z","timestamp":1660721511000},"source":"Crossref","is-referenced-by-count":0,"title":["Typability and Type Inference in Atomic Polymorphism"],"prefix":"10.46298","volume":"Volume 18, Issue 3","author":[{"given":"M. Clarence","family":"Protin","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1447-9764","authenticated-orcid":false,"given":"Gilda","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2022,8,12]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9915\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9915\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:02Z","timestamp":1687292402000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7417"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,12]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(3:22)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2104.13675v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2104.13675v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2104.13675v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2104.13675","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2104.13675","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,8,12]]},"article-number":"7417"}}