{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:45:07Z","timestamp":1759146307526},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":376,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>It has been known for six years that the restriction of Girard's polymorphic system F to <jats:italic>atomic<\/jats:italic> universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of \u201cconvertibility\u201d applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each <jats:italic>\u03b2<\/jats:italic>-reduction step of the full intuitionistic propositional calculus translates into one or more <jats:italic>\u03b2\u03b7<\/jats:italic>-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to <jats:italic>\u03b7<\/jats:italic>-conversions.<\/jats:p>","DOI":"10.2178\/jsl.7801180","type":"journal-article","created":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T14:38:23Z","timestamp":1358951903000},"page":"260-274","source":"Crossref","is-referenced-by-count":13,"title":["Atomic polymorphism"],"prefix":"10.1017","volume":"78","author":[{"given":"Fernando","family":"Ferreira","sequence":"first","affiliation":[]},{"given":"Gilda","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200000402_ref017","volume-title":"Basic proof theory","author":"Troelstra","year":"1996"},{"key":"S0022481200000402_ref016","first-page":"198","volume":"32","author":"Tait","year":"1967","journal-title":"Intentional interpretations of functionals offinite type I"},{"key":"S0022481200000402_ref015","unstructured":"Sandqvist T. , A note on definability of logical operators in second-order logic, unpublished manuscript, 2008."},{"key":"S0022481200000402_ref010","first-page":"28","volume-title":"Proceedings of 15th ACM symposium on principles of programming languages","author":"Mitchell","year":"1988"},{"key":"S0022481200000402_ref008","unstructured":"Kretz M. , On the treatment of predicative polymorphism in theories of explicit mathematics, Ph.D. thesis, Universit\u00e4t Bern, 2002."},{"key":"S0022481200000402_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-002-0156-9"},{"key":"S0022481200000402_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0022481200000402_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-009-9186-1"},{"key":"S0022481200000402_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-9001-z"},{"key":"S0022481200000402_ref011","volume-title":"Natural deduction","author":"Prawitz","year":"1965"},{"key":"S0022481200000402_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_6"},{"key":"S0022481200000402_ref013","volume-title":"Collogue sur la programmation","volume":"19","author":"Reynolds","year":"1974"},{"key":"S0022481200000402_ref009","first-page":"365","volume-title":"Handbook of theoretical computer science","volume":"B","author":"Mitchell","year":"1990"},{"key":"S0022481200000402_ref006","volume-title":"Proofs and types","author":"Girard","year":"1989"},{"key":"S0022481200000402_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.06.002"},{"key":"S0022481200000402_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"S0022481200000402_ref014","volume-title":"Principia mathematica","author":"Russell","year":"1927"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200000402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T19:12:06Z","timestamp":1556133126000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200000402\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["S0022481200000402"],"URL":"https:\/\/doi.org\/10.2178\/jsl.7801180","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3]]}}}