{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:08Z","timestamp":1750306808322,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,11]],"date-time":"2014-01-11T00:00:00Z","timestamp":1389398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,11]]},"DOI":"10.1145\/2541568.2541575","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T13:40:06Z","timestamp":1389706806000},"page":"3-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The recursive polarized dual calculus"],"prefix":"10.1145","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[{"name":"The University of Iowa, Iowa City, IA, USA"}]}],"member":"320","published-online":{"date-parts":[[2014,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"volume-title":"Workshop on Partiality and Recursion in Interactive Theorem Provers. Available from the authors' web pages.","author":"Altenkirch Thorsten","key":"e_1_3_2_1_2_1","unstructured":"Thorsten Altenkirch and Nils Anders Danielsson . Termination Checking Nested Inductive and Coinductive Types. Short note supporting a talk given at PAR 2010 , Workshop on Partiality and Recursion in Interactive Theorem Provers. Available from the authors' web pages. Thorsten Altenkirch and Nils Anders Danielsson. Termination Checking Nested Inductive and Coinductive Types. Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers. Available from the authors' web pages."},{"key":"e_1_3_2_1_3_1","volume-title":"Compiling with Continuations","author":"Appel Andrew W.","year":"1992","unstructured":"Andrew W. Appel . Compiling with Continuations . Cambridge University Press , 1992 . Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_2_1_5_1","volume-title":"On streams that are finitely red. Logical Methods in Computer Science, 8(4)","author":"Bezem Marc","year":"2012","unstructured":"Marc Bezem , Keiko Nakata , and Tarmo Uustalu . On streams that are finitely red. Logical Methods in Computer Science, 8(4) , 2012 . Marc Bezem, Keiko Nakata, and Tarmo Uustalu. On streams that are finitely red. Logical Methods in Computer Science, 8(4), 2012."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003512"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_3_2_1_11_1","volume-title":"Call-by-value and call-by-name dual calculi with inductive and coinductive types. Logical Methods in Computer Science, 9(1)","author":"Kimura Daisuke","year":"2013","unstructured":"Daisuke Kimura and Makoto Tatsuta . Call-by-value and call-by-name dual calculi with inductive and coinductive types. Logical Methods in Computer Science, 9(1) , 2013 . Daisuke Kimura and Makoto Tatsuta. Call-by-value and call-by-name dual calculi with inductive and coinductive types. Logical Methods in Computer Science, 9(1), 2013."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_2_1_13_1","first-page":"197","article-title":"Realizability in classical logic","volume":"27","author":"Krivine Jean-Louis","year":"2009","unstructured":"Jean-Louis Krivine . Realizability in classical logic . Panoramas et synth\u00e8ses , 27 : 197 -- 229 , 2009 . Interactive models of computation and program behaviour. Soci\u00e9t\u00e9 Math\u00e9matique de France. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synth\u00e8ses, 27:197--229, 2009. Interactive models of computation and program behaviour. Soci\u00e9t\u00e9 Math\u00e9matique de France.","journal-title":"Panoramas et synth\u00e8ses"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000132"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/645706.663989"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_15"}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"San Diego California USA","acronym":"POPL '14"},"container-title":["Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2541568.2541575","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2541568.2541575","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:35:02Z","timestamp":1750232102000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2541568.2541575"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,11]]},"references-count":17,"alternative-id":["10.1145\/2541568.2541575","10.1145\/2541568"],"URL":"https:\/\/doi.org\/10.1145\/2541568.2541575","relation":{},"subject":[],"published":{"date-parts":[[2014,1,11]]},"assertion":[{"value":"2014-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}