{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T09:19:42Z","timestamp":1648804782763},"reference-count":22,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T00:00:00Z","timestamp":1583280000000},"content-version":"vor","delay-in-days":63,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,23]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate (co-) induction in classical logic under the propositions-as-types paradigm, considering propositional, second-order and (co-) inductive types. Specifically, we introduce an extension of the Dual Calculus with a Mendler-style (co-) iterator and show that it is strongly normalizing. We prove this using a reducibility argument.<\/jats:p>","DOI":"10.1093\/logcom\/exaa004","type":"journal-article","created":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T20:09:05Z","timestamp":1580587745000},"page":"77-106","source":"Crossref","is-referenced-by-count":1,"title":["Classical logic with Mendler induction"],"prefix":"10.1093","volume":"30","author":[{"given":"Marco","family":"Devesas Campos","sequence":"first","affiliation":[{"name":"Department of Computer Science and Technology, University of Cambridge, CB3 0FD Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[{"name":"Department of Computer Science and Technology, University of Cambridge, CB3 0FD Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2020,3,3]]},"reference":[{"key":"2020040702352979400_ref1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2004.10.017","article-title":"Iteration and coiteration schemes for higher-order and nested datatypes","volume":"333","author":"Abel","year":"2005","journal-title":"Theoretical Computer Science"},{"key":"2020040702352979400_ref2","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/2034773.2034807","article-title":"A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences","volume-title":"Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming","author":"Ahn","year":"2011"},{"key":"2020040702352979400_ref3","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0025","article-title":"A symmetric lambda calculus for classical program extraction","volume":"125,","author":"Barbanera","year":"1996","journal-title":"Information and Computation"},{"key":"2020040702352979400_ref4","first-page":"365","article-title":"\u2018Classical\u2019 programming-with-proofs in $\\lambda ^{Sym}_{PA}$. An analysis of non-confluence","volume-title":"Theoretical Aspects of Computer Software, vol. 1281 of Lecture Notes in Computer Science","author":"Barbanera","year":"1997"},{"key":"2020040702352979400_ref5","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1093\/logcom\/14.4.529","article-title":"A formulae-as-types interpretation of subtractive logic","volume":"14,","author":"Crolard","year":"2004","journal-title":"Journal of Logic and Computation"},{"key":"2020040702352979400_ref6","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/351240.351262","article-title":"The duality of computation","volume-title":"Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming","author":"Curien","year":"2000"},{"key":"2020040702352979400_ref7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"Davey","year":"2002"},{"key":"2020040702352979400_ref8","doi-asserted-by":"crossref","first-page":"65","DOI":"10.2178\/bsl\/1182353853","article-title":"Fixed point logics","volume":"8,","author":"Dawar","year":"2002","journal-title":"Bulletin of Symbolic Logic"},{"key":"2020040702352979400_ref9","volume-title":"Mendler Induction and Classical Logic","author":"Campos","year":"2015"},{"key":"2020040702352979400_ref10","first-page":"169","article-title":"Strong normalization of the dual classical sequent calculus","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, vol. 3835 of Lecture Notes in Computer Science","author":"Dougherty","year":"2005"},{"key":"2020040702352979400_ref11","first-page":"288","article-title":"Investigations into logical deduction","volume":"1","author":"Gentzen","year":"1964","journal-title":"American Philosophical Quarterly"},{"key":"2020040702352979400_ref12","volume-title":"ML with callcc is unsound","author":"Harper","year":"1991"},{"key":"2020040702352979400_ref13","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/2429069.2429093","article-title":"The power of parameterization in coinductive proof","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Hur","year":"2013"},{"key":"2020040702352979400_ref14","first-page":"222","article-title":"A tutorial on (co) algebras and (co) induction","volume":"62","author":"Jacobs","year":"1997","journal-title":"Bulletin-European Association for Theoretical Computer Science"},{"key":"2020040702352979400_ref15","first-page":"224","article-title":"Dual calculus with inductive and coinductive types","volume-title":"Rewriting Techniques and Applications, vol. 5595 of Lecture Notes in Computer Science","author":"Kimura","year":"2009"},{"key":"2020040702352979400_ref16","volume-title":"Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types","author":"Matthes","year":"1998"},{"key":"2020040702352979400_ref17","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","article-title":"Inductive types and type constraints in the second-order lambda calculus","volume":"51,","author":"Mendler","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020040702352979400_ref18","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1145\/44501.45065","article-title":"Abstract types have existential type","volume":"10,","author":"Mitchell","year":"1988","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"2020040702352979400_ref19","first-page":"442","article-title":"Strong normalization of second order symmetric $\\lambda $ calculus","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, vol. 1974 of Lecture Notes in Computer Science","author":"Parigot","year":"2000"},{"key":"2020040702352979400_ref20","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/j.tcs.2006.04.009","article-title":"Investigations on the dual calculus","volume":"360,","author":"Tzevelekos","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"2020040702352979400_ref21","first-page":"343","article-title":"Mendler-style inductive types, categorically","volume":"6","author":"Uustalu","year":"1999","journal-title":"Nordic Journal of Computing"},{"key":"2020040702352979400_ref22","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1145\/944705.944723","article-title":"Call-by-value is dual to call-by-name","volume-title":"Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming","author":"Wadler","year":"2003"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/77\/33016434\/exaa004.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/77\/33016434\/exaa004.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,25]],"date-time":"2021-02-25T08:05:59Z","timestamp":1614240359000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/1\/77\/5775548"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":22,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,3,3]]},"published-print":{"date-parts":[[2020,1,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa004","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,1]]},"published":{"date-parts":[[2020,1]]}}}