Publication
The computational content of atomic polymorphism
| datacite.subject.sdg | 04:Educação de Qualidade | pt_PT |
| dc.contributor.author | Ferreira, Gilda | |
| dc.contributor.author | Vasconcelos, Vasco T | |
| dc.date.accessioned | 2020-03-02T16:17:13Z | |
| dc.date.available | 2020-03-02T16:17:13Z | |
| dc.date.issued | 2019 | |
| dc.description.abstract | We show that the number-theoretic functions de nable in the atomic polymorphic system (Fat) are exactly the extended polynomials. Two proofs of the above result are presented: one reducing the functions' de n- ability problem in Fat to de nability in the simply typed lambda-calculus and other directly adapting Helmut Schwichtenberg's strategy for de nability in the simply typed lambda-calculus to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda-calculus, is emphasized. | pt_PT |
| dc.description.sponsorship | This work was supported by Fundação para a Ciência e a Tecnologia [UID/MAT/ 04561/2013, UID/CEC/00408/2013 and grant SFRH/BPD/93278/2013 to G.F.]. The first author is also grateful to Centro de Matemática, Aplicações Fundamentais e Investigação Operacional and to Large-Scale Informatics Systems Laboratory (Universidade de Lisboa). | pt_PT |
| dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
| dc.identifier.doi | 10.1093/jigpal/jzy076 | pt_PT |
| dc.identifier.eissn | 1368-9894 | |
| dc.identifier.issn | 1367-0751 | |
| dc.identifier.uri | http://hdl.handle.net/10400.2/9415 | |
| dc.language.iso | eng | pt_PT |
| dc.peerreviewed | yes | pt_PT |
| dc.publisher | Oxford Academic - Oxford Journals | pt_PT |
| dc.relation | Teoria da demonstração: abordagem lógico-computacional | |
| dc.subject | Predicative polymorphism | pt_PT |
| dc.subject | Representable functions | pt_PT |
| dc.subject | Lambda-calculus | pt_PT |
| dc.subject | Normalization | pt_PT |
| dc.subject | Beta-equality | pt_PT |
| dc.subject | Extended polynomials | pt_PT |
| dc.title | The computational content of atomic polymorphism | pt_PT |
| dc.type | journal article | |
| dspace.entity.type | Publication | |
| oaire.awardTitle | Teoria da demonstração: abordagem lógico-computacional | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/5876/UID%2FMAT%2F04561%2F2013/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/5876/UID%2FCEC%2F00408%2F2013/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT//SFRH%2FBPD%2F93278%2F2013/PT | |
| oaire.citation.endPage | 638 | pt_PT |
| oaire.citation.issue | 5 | pt_PT |
| oaire.citation.startPage | 625 | pt_PT |
| oaire.citation.title | Logic Journal of the IGPL | pt_PT |
| oaire.citation.volume | 27 | pt_PT |
| oaire.fundingStream | 5876 | |
| oaire.fundingStream | 5876 | |
| person.familyName | Ferreira | |
| person.givenName | Gilda | |
| person.identifier.ciencia-id | 0B1A-81E7-88B1 | |
| person.identifier.orcid | 0000-0003-1447-9764 | |
| person.identifier.rid | H-9953-2013 | |
| person.identifier.scopus-author-id | 14037466100 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | article | pt_PT |
| relation.isAuthorOfPublication | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isAuthorOfPublication.latestForDiscovery | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
| relation.isProjectOfPublication | 790cb869-ff08-40ad-8026-fa89e1020bc0 | |
| relation.isProjectOfPublication | decf6855-f566-40f8-af12-50adc657f065 | |
| relation.isProjectOfPublication | dab4f1a3-08b3-4ccc-8509-1aa421dd896c | |
| relation.isProjectOfPublication.latestForDiscovery | 790cb869-ff08-40ad-8026-fa89e1020bc0 |