{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:32:15Z","timestamp":1740123135999,"version":"3.37.3"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,3,27]],"date-time":"2019-03-27T00:00:00Z","timestamp":1553644800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s11225-019-09858-1","type":"journal-article","created":{"date-parts":[[2019,3,27]],"date-time":"2019-03-27T03:04:16Z","timestamp":1553655856000},"page":"477-507","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism"],"prefix":"10.1007","volume":"108","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6348-5653","authenticated-orcid":false,"given":"Jos\u00e9","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[]},{"given":"Gilda","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,3,27]]},"reference":[{"key":"9858_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10992-005-9001-z","volume":"35","author":"F Ferreira","year":"2006","unstructured":"Ferreira, F., Comments on predicative logic, Journal of Philosophical Logic 35:1\u20138, 2006.","journal-title":"Journal of Philosophical Logic"},{"key":"9858_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s11225-009-9186-1","volume":"92","author":"F Ferreira","year":"2009","unstructured":"Ferreira, F., and G.\u00a0Ferreira, Commuting conversions vs. the standard conversions of the \u201cgood\u201d connectives, Studia Logica 92:63\u201384, 2009.","journal-title":"Studia Logica"},{"issue":"1","key":"9858_CR3","doi-asserted-by":"publisher","first-page":"260","DOI":"10.2178\/jsl.7801180","volume":"78","author":"F Ferreira","year":"2013","unstructured":"Ferreira, F., and G.\u00a0Ferreira, Atomic polymorphism, The Journal of Symbolic Logic 78(1):260\u2013274, 2013.","journal-title":"The Journal of Symbolic Logic"},{"issue":"2","key":"9858_CR4","first-page":"115","volume":"25","author":"G Ferreira","year":"2017","unstructured":"Ferreira, G., Eta-conversions of $${\\bf IPC}$$ implemented in atomic $${\\bf F}$$, Logic Jnl IGPL 25(2):115\u2013130, 2017.","journal-title":"Logic Jnl IGPL"},{"issue":"3","key":"9858_CR5","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1007\/s11225-016-9704-x","volume":"105","author":"G Ferreira","year":"2017","unstructured":"Ferreira, G., Rasiowa\u2013Harrop disjunction property, Studia Logica 105(3):649\u2013664, 2017.","journal-title":"Studia Logica"},{"key":"9858_CR6","doi-asserted-by":"crossref","unstructured":"Ghani, N., $$\\beta \\eta $$-equality for coproducts, in Second International Conference on Typed Lambda Calculi and Applications, TLCA \u201995, Edinburgh, UK, April 10\u201312, 1995, Proceedings, vol. 902 of Lecture Notes in Computer Science, Springer, 1995, pp. 171\u2013185.","DOI":"10.1007\/BFb0014052"},{"key":"9858_CR7","volume-title":"Proofs and Types","author":"J-Y Girard","year":"1989","unstructured":"Girard, J-Y., Y.\u00a0Lafont, and P.\u00a0Taylor, Proofs and Types, Cambridge University Press, Cambridge, 1989."},{"key":"9858_CR8","unstructured":"Kretz, M., On the treatment of predicative polymorphism in theories of explicit mathematics, Ph.D. thesis, Universitat Bern, 2002."},{"issue":"2","key":"9858_CR9","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1006\/inco.1994.1038","volume":"110","author":"D Leivant","year":"1994","unstructured":"Leivant, D., A foundational delineation of poly-time, Information and Computation 110(2):391\u2013420, 1994.","journal-title":"Information and Computation"},{"key":"9858_CR10","doi-asserted-by":"crossref","unstructured":"Lindley, S., Extensional rewriting with sums, in Proc. of 8th International Conference on Typed Lambda Calculi and Applications, vol. 624 of Lecture Notes in Computer Science, Springer, 2007, pp. 255\u2013271.","DOI":"10.1007\/978-3-540-73228-0_19"},{"key":"9858_CR11","first-page":"365","volume-title":"Handbook of Theoretical Computer Science","author":"JC Mitchell","year":"1990","unstructured":"Mitchell, J.\u00a0C., Type systems for programming languages, in J.\u00a0van Leeuwen, (ed.), Handbook of Theoretical Computer Science, Elsevier, Amsterdam, 1990, pp. 365\u2013458."},{"key":"9858_CR12","doi-asserted-by":"crossref","unstructured":"Mitchell, J.\u00a0C., and R.\u00a0Harper, The essence of ML, in Proc. of the 15th ACM Symp. on Principles of Programming Languages, ACM, 1988, pp. 28\u201346.","DOI":"10.1145\/73560.73563"},{"key":"9858_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G Plotkin","year":"1975","unstructured":"Plotkin, G., Call-by-name, call-by-value and the $$\\lambda $$-calculus, Theoretical Computer Science 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"key":"9858_CR14","volume-title":"Natural Deduction. A Proof-Theoretical Study","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm, 1965."},{"key":"9858_CR15","doi-asserted-by":"crossref","unstructured":"Prawitz, D., Ideas and results in proof theory, in Proc. Second Scandinavian Logic Symposium, vol.\u00a063 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1971, pp. 235\u2013307.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"9858_CR16","doi-asserted-by":"crossref","unstructured":"Seely, R. A.\u00a0G., Weak adjointness in proof theory, in Proc. of the Durham Conference on Applications of Sheaves, vol. 753 of Lecture Notes in Mathematics, Springer, 1979, pp. 697\u2013701.","DOI":"10.1007\/BFb0061840"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-019-09858-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-019-09858-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-019-09858-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T12:07:50Z","timestamp":1588766870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-019-09858-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,27]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["9858"],"URL":"https:\/\/doi.org\/10.1007\/s11225-019-09858-1","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2019,3,27]]},"assertion":[{"value":"31 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 March 2019","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}