{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T09:44:20Z","timestamp":1791452660928,"version":"4.3.3"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"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":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,2]]},"abstract":"<jats:p>\n            The concept of syntactical\n            <jats:italic>duality<\/jats:italic>\n            is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof\/test duality proposed by Girard in his 1999 paper on the meaning of logical rules. In detail, starting from the notion of \u201ctest\u201d proposed by Girard, we develop a notion of test for intuitionistic logic and we give a complete deductive system whose computational interpretation is the target language of the call-by-value and call-by-name continuation passing style translations.\n          <\/jats:p>","DOI":"10.1145\/1462179.1462184","type":"journal-article","created":{"date-parts":[[2009,2,25]],"date-time":"2009-02-25T14:44:30Z","timestamp":1235573070000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Proofs, tests and continuation passing style"],"prefix":"10.1145","volume":"10","author":[{"given":"Stefano","family":"Guerrini","sequence":"first","affiliation":[{"name":"Sapienza Universit\u00e0 di Roma, Roma, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Masini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Verona, Verona, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,3,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Languages and Programming. Lecture Notes in Computer Science","volume":"2719","author":"Ariola Z. M.","unstructured":"Ariola , Z. M. and Herbelin , H . 2003. Minimal classical logic and control operators. In Automata , Languages and Programming. Lecture Notes in Computer Science , vol. 2719 . Springer, Berlin, 871--885. Ariola, Z. M. and Herbelin, H. 2003. Minimal classical logic and control operators. In Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2719. Springer, Berlin, 871--885."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA'93)","volume":"664","author":"Barbanera F.","unstructured":"Barbanera , F. and Berardi , S . 1993. Extracting constructive content from classical logic via control-like reductions . In Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA'93) , M. Bezem and J. F. Groote, Eds. Lecture Notes in Computer Science , vol. 664 . Springer, The Netherlands, 45--59. Barbanera, F. and Berardi, S. 1993. Extracting constructive content from classical logic via control-like reductions. In Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA'93), M. Bezem and J. F. Groote, Eds. Lecture Notes in Computer Science, vol. 664. Springer, The Netherlands, 45--59."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS '94)","volume":"789","author":"Barbanera F.","unstructured":"Barbanera , F. and Berardi , S . 1994. A symmetric lambda-calculus for classical program extraction . In Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS '94) . Lecture Notes in Computer Science , vol. 789 . Springer. Barbanera, F. and Berardi, S. 1994. A symmetric lambda-calculus for classical program extraction. In Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS '94). Lecture Notes in Computer Science, vol. 789. Springer."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Danos V. Joinet J.-B. and Schellinx H. 1995. LKT and LKQ: Sequent calculi for second order logic based upon dual linear decomposition of classical implication. In Advances in Linear Logic J.-Y. Girard et al. Eds. Cambridge University Press 43--59.  Danos V. Joinet J.-B. and Schellinx H. 1995. LKT and LKQ: Sequent calculi for second order logic based upon dual linear decomposition of classical implication. In Advances in Linear Logic J.-Y. Girard et al. Eds. Cambridge University Press 43--59.","DOI":"10.1017\/CBO9780511629150.011"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 4th ACM SIGPLAN Continuations Workshop (CW'04)","author":"Danvy O.","year":"2004","unstructured":"Danvy , O. 2004 . On evaluation contexts, continuations, and the rest of the computation . In Proceedings of the 4th ACM SIGPLAN Continuations Workshop (CW'04) , H. Thielecke, Ed. Tech. rep. CSR-040-1. Danvy, O. 2004. On evaluation contexts, continuations, and the rest of the computation. In Proceedings of the 4th ACM SIGPLAN Continuations Workshop (CW'04), H. Thielecke, Ed. Tech. rep. CSR-040-1."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002667"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 1st Annual IEEE Sympoisum on Logic in Computer Science (LICS'86)","author":"Felleisen M.","unstructured":"Felleisen , M. , Friedman , D. P. , Kohlbecker , E. E. , and Duba , B. F . 1986. Reasoning with continuations . In Proceedings of the 1st Annual IEEE Sympoisum on Logic in Computer Science (LICS'86) , A. Meyer, Ed. IEEE Computer Society Press, 131--141. Felleisen, M., Friedman, D. P., Kohlbecker, E. E., and Duba, B. F. 1986. Reasoning with continuations. In Proceedings of the 1st Annual IEEE Sympoisum on Logic in Computer Science (LICS'86), A. Meyer, Ed. IEEE Computer Society Press, 131--141."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/800235.807077"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.001"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 1997 NATO Advanced Study Institute on Computational Logic, U. Berger and H. Schwichtenberg, Eds. NATO ASI Series, Computer and Systems Sciences","volume":"165","author":"Girard J.-Y.","year":"1999","unstructured":"Girard , J.-Y. 1999 . On the meaning of logical rules I: Syntax vs. semantics . In Proceedings of the 1997 NATO Advanced Study Institute on Computational Logic, U. Berger and H. Schwichtenberg, Eds. NATO ASI Series, Computer and Systems Sciences , vol. 165 . Springer, 215--272. Girard, J.-Y. 1999. On the meaning of logical rules I: Syntax vs. semantics. In Proceedings of the 1997 NATO Advanced Study Institute on Computational Logic, U. Berger and H. Schwichtenberg, Eds. NATO ASI Series, Computer and Systems Sciences, vol. 165. Springer, 215--272."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_2_1_14_1","unstructured":"Herbelin H. 1995. S\u00e9quents qu'on calcule. Th\u00e8se de Doctorat Universit\u00e9 Paris 7.  Herbelin H. 1995. S\u00e9quents qu'on calcule. Th\u00e8se de Doctorat Universit\u00e9 Paris 7."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)","author":"Hofmann M.","unstructured":"Hofmann , M. and Streicher , T . 1997. Continuation models are universal for lambda-mu-calculus . In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97) . IEEE Computer Society, Washington, DC, 387. Hofmann, M. and Streicher, T. 1997. Continuation models are universal for lambda-mu-calculus. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97). IEEE Computer Society, Washington, DC, 387."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737405"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263722"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645706.663989"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003141"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_15"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(74)90010-2"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462179.1462184","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1462179.1462184","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:15Z","timestamp":1750253415000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462179.1462184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["10.1145\/1462179.1462184"],"URL":"https:\/\/doi.org\/10.1145\/1462179.1462184","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]},"assertion":[{"value":"2006-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}