{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:32:17Z","timestamp":1740123137830,"version":"3.37.3"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T00:00:00Z","timestamp":1513728000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Tr1112\/1-3"],"award-info":[{"award-number":["Tr1112\/1-3"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s11225-017-9772-6","type":"journal-article","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T03:18:10Z","timestamp":1513739890000},"page":"195-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["The Naturality of Natural Deduction"],"prefix":"10.1007","volume":"107","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2844-129X","authenticated-orcid":false,"given":"Luca","family":"Tranchini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Pistone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mattia","family":"Petrolo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,20]]},"reference":[{"key":"9772_CR1","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1017\/S0960129501003309","volume":"11","author":"P Aczel","year":"2001","unstructured":"Aczel, P., The Russell-Prawitz modality, Mathematical Structures in Computer Science 11: 541\u2013554, 2001.","journal-title":"Mathematical Structures in Computer Science"},{"key":"9772_CR2","first-page":"303","volume-title":"Normalization by evaluation for typed lambda calculus with coproducts, in 16th Annual IEEE Symposium on Logic in Computer Science","author":"T Altenkirch","year":"2001","unstructured":"Altenkirch, T., P. Dybjer, M. Hoffman, and P.\u00a0J. Scott, Normalization by evaluation for typed lambda calculus with coproducts, in 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachussetts, 2001, pp. 303\u2013310."},{"key":"9772_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"ES Bainbridge","year":"1990","unstructured":"Bainbridge, E.S., P.\u00a0J. Freyd, A. Scedrov, and P.\u00a0J. Scott, Functorial polymorphism, Theoretical Computer Science 70: 35\u201364, 1990.","journal-title":"Theoretical Computer Science"},{"key":"9772_CR4","first-page":"267","volume-title":"Dinatural terms in System F, in 24th Annual IEEE Symposium on Logic in Computer Science","author":"J Lataillade de","year":"2009","unstructured":"de\u00a0Lataillade, J., Dinatural terms in System F, in 24th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Los Angeles, California, USA, 2009, pp. 267\u2013276."},{"issue":"1","key":"9772_CR5","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. Ferreira, Commuting conversions vs. the standard conversions of the \u201cgood\u201d connectives, Studia Logica 92(1): 63\u201384, 2009.","journal-title":"Studia Logica"},{"issue":"1","key":"9772_CR6","doi-asserted-by":"publisher","first-page":"260","DOI":"10.2178\/jsl.7801180","volume":"78","author":"F Ferreira","year":"2013","unstructured":"Ferreira, F., and G. Ferreira, Atomic polymorphism, Journal of Symbolic Logic 78(1): 260\u2013274, 2013.","journal-title":"Journal of Symbolic Logic"},{"key":"9772_CR7","doi-asserted-by":"crossref","unstructured":"Freyd, P.\u00a0J., J.-Y. Girard, A. Scedrov, and P.\u00a0J. Scott, Semantic parametricity in the polymorphic lambda calculus, in LICS \u201988., Proceedings of the Third Annual Symposium on Logic in Computer Science, IEEE, 1988, pp. 274\u2013279.","DOI":"10.1109\/LICS.1988.5126"},{"key":"9772_CR8","doi-asserted-by":"crossref","unstructured":"Ghani, N., $$\\beta \\eta $$ \u03b2 \u03b7 -equality for coproducts, in TLCA \u201995, International Conference on Typed Lambda Calculi and Applications, vol. 902 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 171\u2013185.","DOI":"10.1007\/BFb0014052"},{"key":"9772_CR9","volume-title":"and P","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y., Y. Lafont, and P. Taylor, Proof and Types, Cambridge University Press, 1989."},{"key":"9772_CR10","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y., A. Scedrov, and P.\u00a0J. Scott, Normal forms and cut-free proofs as natural transformations, in Y.\u00a0Moschovakis, (ed.), Logic from Computer Science, vol.\u00a021 of Mathematical Sciences Research Institute Publications, Springer-Verlag, 1992, pp. 217\u2013241.","DOI":"10.1007\/978-1-4612-2822-6_8"},{"key":"9772_CR11","unstructured":"Lindley, S., Extensional rewriting with sums, in Typed Lambda Calculi and Applications, TLCA 2007, vol. 4583 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2007, pp. 255\u2013271."},{"key":"9772_CR12","unstructured":"Prawitz, D., Natural deduction, a proof-theoretical study, Almqvist & Wiskell, 1965."},{"key":"9772_CR13","doi-asserted-by":"crossref","unstructured":"Prawitz, D., Ideas and results in proof theory, in J.E. Fenstad, (ed.), Proceedings of the 2nd Scandinavian Logic Symposium (Oslo), Studies in logic and foundations of mathematics, vol.\u00a063, North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"9772_CR14","unstructured":"Prawitz, D., Proofs and the meaning and completeness of the logical constants, in J. Hintikka, I. Niiniluoto, and E. Saarinen, (eds.), Essays on Mathematical and Philosophical Logic: Proceedings of the Fourth Scandinavian Logic Symposium and the First Soviet-Finnish Logic Conference, Jyv\u00e4skyl\u00e4, Finland, June 29\u2013July 6, 1976, Kluwer, Dordrecht, 1979, pp. 25\u201340."},{"key":"9772_CR15","unstructured":"Russell, B., The Principles of Mathematics, George Allen and Unwin Ltd. (2nd edition 1937), 1903."},{"issue":"4","key":"9772_CR16","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P., A natural extension of natural deduction, Journal of Symbolic Logic 49(4): 1284\u20131300, 1984.","journal-title":"Journal of Symbolic Logic"},{"issue":"6","key":"9772_CR17","doi-asserted-by":"publisher","first-page":"1185","DOI":"10.1007\/s11225-014-9562-3","volume":"102","author":"P Schroeder-Heister","year":"2014","unstructured":"Schroeder-Heister, P., The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony, Studia Logica 102(6): 1185\u20131216, 2014.","journal-title":"Studia Logica"},{"key":"9772_CR18","volume-title":"and A","author":"H Schwichtenberg","year":"2000","unstructured":"Schwichtenberg, H., and A. S. Troelstra, Basic proof theory, Cambridge University Press, 2000."},{"key":"9772_CR19","doi-asserted-by":"crossref","unstructured":"Seely, R. A.\u00a0G., Weak adjointness in proof theory, in Proceedings of the Durham Conference on Applications of Sheaves, vol. 753 of Springer Lecture Notes in Mathematics, Springer Berlin, 1979, pp. 697\u2013701.","DOI":"10.1007\/BFb0061840"},{"key":"9772_CR20","doi-asserted-by":"publisher","unstructured":"Tranchini, L., Proof-theoretic harmony: Towards an intensional account, Synthese, Online first (2016). https:\/\/doi.org\/10.1007\/s11229-016-1200-3 .","DOI":"10.1007\/s11229-016-1200-3"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-017-9772-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-017-9772-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-017-9772-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,24]],"date-time":"2020-10-24T14:47:51Z","timestamp":1603550871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-017-9772-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,20]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["9772"],"URL":"https:\/\/doi.org\/10.1007\/s11225-017-9772-6","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2017,12,20]]},"assertion":[{"value":"20 December 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}