{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:54:13Z","timestamp":1743119653856,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319276823"},{"type":"electronic","value":"9783319276830"}],"license":[{"start":{"date-parts":[[2015,12,10]],"date-time":"2015-12-10T00:00:00Z","timestamp":1449705600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-27683-0_4","type":"book-chapter","created":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T16:16:29Z","timestamp":1449677789000},"page":"43-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Classical Logic with Mendler Induction"],"prefix":"10.1007","author":[{"given":"Marco","family":"Devesas Campos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo","family":"Fiore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,10]]},"reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2004.10.017","volume":"333","author":"A Abel","year":"2005","unstructured":"Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333(1), 3\u201366 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Ahn, K.Y., Sheard, T.: A hierarchy of Mendler style recursion combinators: Taming inductive datatypes with negative occurrences. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 234\u2013246. ACM, New York (2011)","DOI":"10.1145\/2034773.2034807"},{"issue":"2","key":"4_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Inf. Comput. 125(2), 103\u2013117 (1996)","journal-title":"Inf. Comput."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BFb0014559","volume-title":"Theoretical Aspects of Computer Software","author":"F Barbanera","year":"1997","unstructured":"Barbanera, F., Berardi, S., Schivalocchi, M.: \u201cClassical\u201d programming-with-proofs in \n                    \n                      \n                    \n                    $$\\lambda ^{Sym}_{PA}$$\n                   : An analysis of non-confluence. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, vol. 1281, pp. 365\u2013390. Springer, Berlin Heidelberg (1997)"},{"issue":"4","key":"4_CR5","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1093\/logcom\/14.4.529","volume":"14","author":"T Crolard","year":"2004","unstructured":"Crolard, T.: A formulae-as-types interpretation of subtractive logic. J. Log. Comput. 14(4), 529\u2013570 (2004)","journal-title":"J. Log. Comput."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Curien, P.L., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming ICFP 2000, pp. 233\u2013243. ACM, New York (2000)","DOI":"10.1145\/357766.351262"},{"key":"4_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"2002","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)"},{"issue":"01","key":"4_CR8","doi-asserted-by":"publisher","first-page":"65","DOI":"10.2178\/bsl\/1182353853","volume":"8","author":"A Dawar","year":"2002","unstructured":"Dawar, A., Gurevich, Y.: Fixed point logics. Bull. Symb. Log. 8(01), 65\u201388 (2002)","journal-title":"Bull. Symb. Log."},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11591191_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"DJ Dougherty","year":"2005","unstructured":"Dougherty, D.J., Ghilezan, S., Lescanne, P., Likavec, S.: Strong normalization of the dual classical sequent calculus. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 169\u2013183. Springer, Heidelberg (2005)"},{"issue":"4","key":"4_CR10","first-page":"288","volume":"1","author":"G Gentzen","year":"1964","unstructured":"Gentzen, G.: Investigations into logical deduction. Am. Philos. Q. 1(4), 288\u2013306 (1964)","journal-title":"Am. Philos. Q."},{"key":"4_CR11","unstructured":"Harper, B., Lillibridge, M.: ML with callcc is unsound. Post to TYPES mailing list (1991)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2013, pp. 193\u2013206. ACM, New York (2013)","DOI":"10.1145\/2480359.2429093"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-02348-4_16","volume-title":"Rewriting Techniques and Applications","author":"D Kimura","year":"2009","unstructured":"Kimura, D., Tatsuta, M.: Dual Calculus with inductive and coinductive types. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 224\u2013238. Springer, Heidelberg (2009)"},{"key":"4_CR14","unstructured":"Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. thesis, Ludwig-Maximilians Universit\u00e4t, May 1998"},{"issue":"1","key":"4_CR15","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N Mendler","year":"1991","unstructured":"Mendler, N.: Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Log. 51(1), 159\u2013172 (1991)","journal-title":"Ann. Pure Appl. Log."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-44450-5_36","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"M Parigot","year":"2000","unstructured":"Parigot, M.: Strong normalization of second order symmetric \n                    \n                      \n                    \n                    $$\\lambda $$\n                  -calculus. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 442\u2013453. Springer, Heidelberg (2000)"},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/j.tcs.2006.04.009","volume":"360","author":"N Tzevelekos","year":"2006","unstructured":"Tzevelekos, N.: Investigations on the Dual Calculus. Theor. Comput. Sci. 360(1), 289\u2013326 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"4_CR18","first-page":"343","volume":"6","author":"T Uustalu","year":"1999","unstructured":"Uustalu, T., Vene, V.: Mendler-style inductive types, categorically. Nord. J. Comput. 6(3), 343 (1999)","journal-title":"Nord. J. Comput."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Call-by-value is dual to call-by-name. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming ICFP 2003, pp. 189\u2013201. ACM, New York (2003)","DOI":"10.1145\/944746.944723"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27683-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T06:28:41Z","timestamp":1578551321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27683-0_4"}},"subtitle":["A Dual Calculus and Its Strong Normalization"],"short-title":[],"issued":{"date-parts":[[2015,12,10]]},"ISBN":["9783319276823","9783319276830"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27683-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,10]]},"assertion":[{"value":"10 December 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}