{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:10Z","timestamp":1750307710905,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T00:00:00Z","timestamp":1232409600000},"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":[[2009,1,20]]},"DOI":"10.1145\/1481848.1481852","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"page":"15-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Refinement types and computational duality"],"prefix":"10.1145","author":[{"given":"Noam","family":"Zeilberger","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]}],"member":"320","published-online":{"date-parts":[[2009,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.16"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01621472"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"volume-title":"CW'04: Proceedings of the Fourth ACM-SIGPLAN Continuation Workshop","year":"2004","author":"Danvy Olivier","key":"e_1_3_2_1_7_1"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"volume-title":"University of Copenhagen","year":"1989","author":"Filinski Andrzej","key":"e_1_3_2_1_10_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_3_2_1_13_1","unstructured":"Bob Harper and Mark Lillibridge. ML with callcc is unsound 1991. Post to TYPES mailing list July 8 1991 archived at http:\/\/www.seas.upenn.edu\/ sweirich\/types\/archive\/1991\/msg00034.html.  Bob Harper and Mark Lillibridge. ML with callcc is unsound 1991. Post to TYPES mailing list July 8 1991 archived at http:\/\/www.seas.upenn.edu\/ sweirich\/types\/archive\/1991\/msg00034.html."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351242"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139171472"},{"key":"e_1_3_2_1_16_1","unstructured":"S\u00f8ren\n     B.\n      \n  \n   \n  Lassen and Paul Blain Levy. Typed normal form bisimulation. In Jacques Duparc and Thomas A. Henzinger editors CSL volume \n  4646\n   of \n  Lecture Notes in Computer Science pages \n  283\n  --\n  297\n  . \n  Springer 2007\n  .   S\u00f8ren B. Lassen and Paul Blain Levy. Typed normal form bisimulation. In Jacques Duparc and Thomas A. Henzinger editors CSL volume 4646 of Lecture Notes in Computer Science pages 283--297. Springer 2007."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.42"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01091743"},{"volume-title":"Chalmers University of Technology","year":"2007","author":"Norell Ulf","key":"e_1_3_2_1_20_1"},{"volume-title":"Studies in Logic and the Foundations of Mathematics","year":"2008","author":"Pfenning Frank","key":"e_1_3_2_1_21_1"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111047"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"issue":"1","key":"e_1_3_2_1_26_1","article-title":"On the unity of duality","volume":"153","author":"Zeilberger Noam","year":"2008","journal-title":"Annals of Pure and Applied Logic"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328482"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Savannah GA USA","acronym":"POPL09"},"container-title":["Proceedings of the 3rd workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481852","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481848.1481852","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:10Z","timestamp":1750253410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,20]]},"references-count":26,"alternative-id":["10.1145\/1481848.1481852","10.1145\/1481848"],"URL":"https:\/\/doi.org\/10.1145\/1481848.1481852","relation":{},"subject":[],"published":{"date-parts":[[2009,1,20]]},"assertion":[{"value":"2009-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}