{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:37:14Z","timestamp":1740141434552,"version":"3.37.3"},"reference-count":16,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T00:00:00Z","timestamp":1544054400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["UID\/MAT\/04561\/2013","UID\/CEC\/00408\/2013","SFRH\/BPD\/93278\/2013"],"award-info":[{"award-number":["UID\/MAT\/04561\/2013","UID\/CEC\/00408\/2013","SFRH\/BPD\/93278\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007690","name":"Centro de Matem\u00e1tica e Aplica\u00e7\u00f5es da Universidade da Beira Interior","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100007690","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,9,25]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that the number-theoretic functions definable in the atomic polymorphic system (${\\mathbf{F}}_{\\mathbf{at}}$) are exactly the extended polynomials. Two proofs of the above result are presented: one, reducing the functions\u2019 definability problem in ${\\mathbf{F}}_{\\mathbf{at}}$ to definability in the simply typed lambda calculus ($\\lambda ^{\\rightarrow }$) and the other, directly adapting Helmut Schwichtenberg\u2019s strategy for definability in $\\lambda ^{\\rightarrow }$ to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda calculus, is emphasized.<\/jats:p>","DOI":"10.1093\/jigpal\/jzy076","type":"journal-article","created":{"date-parts":[[2018,11,13]],"date-time":"2018-11-13T20:16:30Z","timestamp":1542140190000},"page":"625-638","source":"Crossref","is-referenced-by-count":1,"title":["The computational content of atomic polymorphism"],"prefix":"10.1093","volume":"27","author":[{"given":"Gilda","family":"Ferreira","sequence":"first","affiliation":[{"name":"Universidade Aberta, Rua Braamcamp, 90, Lisboa, Portugal"}]},{"given":"Vasco T","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"LaSIGE, Departamento de Inform\u00e1tica, Faculdade de Ci\u00eancias da Universidade de Lisboa Campo Grande, Ed. C6, Lisboa, Portugal"}]}],"member":"286","published-online":{"date-parts":[[2018,12,6]]},"reference":[{"key":"2019100107220076900_ref1","first-page":"1","article-title":"An elementary fragment of second-order lambda-calculus","volume-title":"ACM Transactions on Computational Logic, V","author":"Aehlig","year":"2004"},{"key":"2019100107220076900_ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10992-005-9001-z","article-title":"Comments on predicative logic","volume":"35","author":"Ferreira","year":"2006","journal-title":"Journal of Philosophical Logic"},{"key":"2019100107220076900_ref3","doi-asserted-by":"crossref","first-page":"260","DOI":"10.2178\/jsl.7801180","article-title":"Atomic polymorphism","volume":"78","author":"Ferreira","year":"2013","journal-title":"The Journal of Symbolic Logic"},{"key":"2019100107220076900_ref4","first-page":"1303","article-title":"The faithfulness of ${\\mathbf{F}}_{\\mathbf{at}}$: a proof-theoretic proof","volume-title":"Studia Logica","author":"Ferreira","year":"2015"},{"key":"2019100107220076900_ref5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.18778\/0138-0680.45.1.01","article-title":"An elementary proof of strong normalization for atomic $\\mathbf{F}$","volume":"45","author":"Ferreira","year":"2016","journal-title":"Bulletin of the Section of Logic"},{"key":"2019100107220076900_ref6","doi-asserted-by":"crossref","first-page":"649","DOI":"10.1007\/s11225-016-9704-x","article-title":"Rasiowa\u2013Harrop disjunction property","volume":"105","author":"Ferreira","year":"2017","journal-title":"Studia Logica"},{"key":"2019100107220076900_ref7","first-page":"115","article-title":"Eta-conversions of $\\mathbf{IPC}$ implemented in atomic $\\mathbf{F}$","volume":"25","author":"Ferreira","year":"2017","journal-title":"Logic Journal of the IGPL"},{"key":"2019100107220076900_ref8","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","article-title":"The expressiveness of simple and second-order type structures","volume":"30","author":"Fortune","year":"1983","journal-title":"Journal of the Association for Computing Machinery"},{"volume-title":"Proofs and Types","year":"1989","author":"Girard","key":"2019100107220076900_ref9"},{"key":"2019100107220076900_ref10","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0890-5401(91)90053-5","article-title":"Finitely stratified polymorphism","volume":"93","author":"Leivant","year":"1991","journal-title":"Information and Computation"},{"key":"2019100107220076900_ref11","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1006\/inco.1994.1038","article-title":"A foundational delineation of poly-time","volume":"110","author":"Leivant","year":"1994","journal-title":"Information and Computation"},{"author":"Pistone","key":"2019100107220076900_ref12","article-title":"Proof nets and the instantiation overflow property"},{"key":"2019100107220076900_ref13","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF02276799","article-title":"Definierbare Funktionen im $\\lambda$-kalk\u00fcl Mit Typen","volume":"17","author":"Schwichtenberg","year":"1976","journal-title":"Archive for Mathematical Logik"},{"key":"2019100107220076900_ref14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/SFCS.1981.24","article-title":"Number theoretic functions computable by polynomial programs (extended abstract)","author":"Statman","year":"1981","journal-title":"Proceedings 22nd IEEE Annual Symposium on Foundation of Computer Science"},{"key":"2019100107220076900_ref15","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","article-title":"The typed $\\lambda$-calculus is not elementary recursive","volume":"9","author":"Statman","year":"1979","journal-title":"Theoretical Computer Science"},{"key":"2019100107220076900_ref16","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/27\/5\/625\/30073780\/jzy076.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,15]],"date-time":"2020-11-15T05:12:49Z","timestamp":1605417169000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/27\/5\/625\/5230063"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,6]]},"references-count":16,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2018,12,6]]},"published-print":{"date-parts":[[2019,9,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzy076","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2019,10]]},"published":{"date-parts":[[2018,12,6]]}}}