{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:15Z","timestamp":1750220835493,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T00:00:00Z","timestamp":1566086400000},"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":[[2019,8,18]]},"DOI":"10.1145\/3331554.3342605","type":"proceedings-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:51:45Z","timestamp":1564433505000},"page":"27-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Deferring the details and deriving programs"],"prefix":"10.1145","author":[{"given":"Liam","family":"O'Connor","sequence":"first","affiliation":[{"name":"UNSW, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,8,18]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Guillaume Allais. 2015. Presburger Arithmetic Solver for Agda. https: \/\/github.com\/gallais\/agda-presburger .  Guillaume Allais. 2015. Presburger Arithmetic Solver for Agda. https: \/\/github.com\/gallais\/agda-presburger ."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_3_2_2_4_1","volume-title":"The essence of ornaments. Journal of Functional Programming 27","author":"Dagand Pierre-Evariste","year":"2017","unstructured":"Pierre-Evariste Dagand . 2017. The essence of ornaments. Journal of Functional Programming 27 ( 2017 ). Pierre-Evariste Dagand. 2017. The essence of ornaments. Journal of Functional Programming 27 (2017)."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364544"},{"volume-title":"Proceedings of the 31st International Conference on Software Engineering (ICSE \u201909)","author":"Dahlweid M.","key":"e_1_3_2_2_6_1","unstructured":"M. Dahlweid , M. Moskal , T. Santen , S. Tobies , and W. Schulte . 2009. VCC: Contract-based modular verification of concurrent C . In Proceedings of the 31st International Conference on Software Engineering (ICSE \u201909) . 429\u2013430. M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte. 2009. VCC: Contract-based modular verification of concurrent C. In Proceedings of the 31st International Conference on Software Engineering (ICSE \u201909). 429\u2013430."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122968"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273307"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","key":"e_1_3_2_2_10_1","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice Hall PTR , Upper Saddle River, NJ, USA. Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall PTR, Upper Saddle River, NJ, USA."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803418"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_2_15_1","volume-title":"Bridging the Gap: Automatic Verified Abstraction of C. In International Conference on Interactive Theorem Proving, Lennart Beringer and Amy Felty (Ed.). Springer","author":"Greenaway David","year":"2012","unstructured":"David Greenaway , June Andronick , and Gerwin Klein . 2012 . Bridging the Gap: Automatic Verified Abstraction of C. In International Conference on Interactive Theorem Proving, Lennart Beringer and Amy Felty (Ed.). Springer , Princeton, New Jersey, USA, 99\u2013115. David Greenaway, June Andronick, and Gerwin Klein. 2012. Bridging the Gap: Automatic Verified Abstraction of C. In International Conference on Interactive Theorem Proving, Lennart Beringer and Amy Felty (Ed.). Springer, Princeton, New Jersey, USA, 99\u2013115."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512782"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_19_1","unstructured":"INRIA. 2009. The Coq Proof Assistant Reference Manual.  INRIA. 2009. The Coq Proof Assistant Reference Manual."},{"key":"e_1_3_2_2_20_1","unstructured":"Wojciech Jedynak. 2015. Ring Solver for Agda. https:\/\/github.com\/ wjzz\/Agda-reflection-for-semiring-solver .  Wojciech Jedynak. 2015. Ring Solver for Agda. https:\/\/github.com\/ wjzz\/Agda-reflection-for-semiring-solver ."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_23_1","volume-title":"Programming with ornaments. Journal of Functional Programming 27","author":"Ko Hsiang-Shang","year":"2016","unstructured":"Hsiang-Shang Ko and Jeremy Gibbons . 2016. Programming with ornaments. Journal of Functional Programming 27 ( 2016 ). Hsiang-Shang Ko and Jeremy Gibbons. 2016. Programming with ornaments. Journal of Functional Programming 27 (2016)."},{"volume-title":"Mathematics of Program Construction, Ralf Hinze and Janis Voigtl\u00e4nder (Eds.)","author":"Kokke Pepijn","key":"e_1_3_2_2_24_1","unstructured":"Pepijn Kokke and Wouter Swierstra . 2015. Auto in Agda . In Mathematics of Program Construction, Ralf Hinze and Janis Voigtl\u00e4nder (Eds.) . Springer International Publishing , Cham , 276\u2013301. Pepijn Kokke and Wouter Swierstra. 2015. Auto in Agda. In Mathematics of Program Construction, Ralf Hinze and Janis Voigtl\u00e4nder (Eds.). Springer International Publishing, Cham, 276\u2013301."},{"key":"e_1_3_2_2_25_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M . Clarke and Andrei Voronkov (Eds.). Springer Berlin Heidelberg , 348\u2013370. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, 348\u2013370."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_10"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628144"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976007"},{"key":"e_1_3_2_2_30_1","unstructured":"Conor McBride. 2010. Ornamental Algebras Algebraic Ornaments. (2010). http:\/\/personal.cis.strath.ac.uk\/~conor\/pub\/OAAO\/Ornament. pdf Manuscript available online.  Conor McBride. 2010. Ornamental Algebras Algebraic Ornaments. (2010). http:\/\/personal.cis.strath.ac.uk\/~conor\/pub\/OAAO\/Ornament. pdf Manuscript available online."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628163"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_2_33_1","volume-title":"Programming from Specifications","author":"Morgan Carroll","unstructured":"Carroll Morgan . 1994. Programming from Specifications ( 2 nd Ed.). Prentice Hall International Ltd . Carroll Morgan. 1994. Programming from Specifications (2nd Ed.). Prentice Hall International Ltd.","edition":"2"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence Paulson and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Vol. 2283.   Tobias Nipkow Lawrence Paulson and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Vol. 2283.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976030"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752639"},{"key":"e_1_3_2_2_38_1","volume-title":"Pearce and Lindsay Groves","author":"David","year":"2013","unstructured":"David J. Pearce and Lindsay Groves . 2013 . Whiley : A Platform for Research in Software Verification. In Software Language Engineering, Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.). Springer International Publishing , Cham, 238\u2013248. David J. Pearce and Lindsay Groves. 2013. Whiley: A Platform for Research in Software Verification. In Software Language Engineering, Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.). Springer International Publishing, Cham, 238\u2013248."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.27"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"volume-title":"Logic for Programming","author":"Schirmer Norbert","key":"e_1_3_2_2_41_1","unstructured":"Norbert Schirmer . 2005. A Verification Environment for Sequential Imperative Programs in Isabelle\/HOL . In Logic for Programming , Artificial Intelligence, and Reasoning, Franz Baader and Andrei Voronkov (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 398\u2013414. Norbert Schirmer. 2005. A Verification Environment for Sequential Imperative Programs in Isabelle\/HOL. In Logic for Programming, Artificial Intelligence, and Reasoning, Franz Baader and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 398\u2013414."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1789277.1789293"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158109"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"}],"event":{"name":"ICFP '19: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Berlin Germany","acronym":"ICFP '19"},"container-title":["Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331554.3342605","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331554.3342605","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:39Z","timestamp":1750202019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331554.3342605"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,18]]},"references-count":46,"alternative-id":["10.1145\/3331554.3342605","10.1145\/3331554"],"URL":"https:\/\/doi.org\/10.1145\/3331554.3342605","relation":{},"subject":[],"published":{"date-parts":[[2019,8,18]]},"assertion":[{"value":"2019-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}