{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T09:36:29Z","timestamp":1761989789443,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T00:00:00Z","timestamp":1726790400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Royal Society of New Zealand Marsden Fund","award":["VUW1812, CRP2101"],"award-info":[{"award-number":["VUW1812, CRP2101"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,20]]},"DOI":"10.1145\/3678721.3686228","type":"proceedings-article","created":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T07:02:52Z","timestamp":1726210972000},"page":"37-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Dafny vs. Dala: Experience with Mechanising Language Design"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-5692","authenticated-orcid":false,"given":"James","family":"Noble","sequence":"first","affiliation":[{"name":"Creative Research & Programming, Wellington, New Zealand \/ Australian National University, Canberra, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3098-3901","authenticated-orcid":false,"given":"Julian","family":"Mackay","sequence":"additional","affiliation":[{"name":"Victoria University of Wellington, Wellington, New Zealand"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4269-5408","authenticated-orcid":false,"given":"Tobias","family":"Wrigstad","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0078-7327","authenticated-orcid":false,"given":"Andrew","family":"Fawcet","sequence":"additional","affiliation":[{"name":"Victoria University of Wellington, Wellington, New Zealand"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0280-6748","authenticated-orcid":false,"given":"Michael","family":"Homer","sequence":"additional","affiliation":[{"name":"Victoria University of Wellington, Wellington, New Zealand"}]}],"member":"320","published-online":{"date-parts":[[2024,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Learning Rust: How Experienced Programmers Leverage Resources to Learn a New Programming Language. In CHI Extended Abstracts. 1\u20138.","author":"Abtahi Parastoo","year":"2020","unstructured":"Parastoo Abtahi and Griffin Dietz. 2020. Learning Rust: How Experienced Programmers Leverage Resources to Learn a New Programming Language. In CHI Extended Abstracts. 1\u20138."},{"key":"e_1_3_2_1_2_1","unstructured":"Amazon. 2023. Automated reasoning. https:\/\/www.amazon.science\/research-areas\/automated-reasoning [Online] [Accessed: 2023-04-20]"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings 12th SIGPLAN Symp. on New Ideas in Programming and Reflections on Software. ACM","author":"Black Andrew P.","year":"2012","unstructured":"Andrew P. Black, Kim B. Bruce, Michael Homer, and James Noble. 2012. Grace: the absence of (inessential) difficulty. In Onward! \u201912: Proceedings 12th SIGPLAN Symp. on New Ideas in Programming and Reflections on Software. ACM, New York, NY. 85\u201398."},{"key":"e_1_3_2_1_5_1","unstructured":"David Blaser. 2019. Simple Explanation of Complex Lifetime Errors in Rust. ETH Z\u00fcrich"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.370"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_3_2_1_8_1","volume-title":"FM 2023, L\u00fcbeck, Germany, March 6-10, 2023, Proceedings, Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.) (Lecture Notes in Computer Science","volume":"583","author":"Cassez Franck","year":"2023","unstructured":"Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio Mijail Anton Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods - 25th International Symposium, FM 2023, L\u00fcbeck, Germany, March 6-10, 2023, Proceedings, Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.) (Lecture Notes in Computer Science, Vol. 14000). Springer, 571\u2013583."},{"key":"e_1_3_2_1_9_1","unstructured":"Elias Castegren and Tobias Wrigstad. 2016. Reference Capabilities for Concurrency Control. In ECOOP."},{"key":"e_1_3_2_1_10_1","unstructured":"Elias Castegren and Tobias Wrigstad. 2016. Reference Capabilities for Trait Based Reuse and Concurrency Control."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_23"},{"key":"e_1_3_2_1_12_1","unstructured":"David Chisnall Matthew Parkinson and Sylvan Clebsch. 2021. Project Verona. www.microsoft.com\/en-us\/research\/project\/project-verona"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"David Clarke John M. Potter and James Noble. 1998. Ownership Types for Flexible Alias Protection. In OOPSLA.","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Sylvan Clebsch. 2015. Deny capabilities for safe fast actors. In AGERE. 1\u201312.","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Michael J. Coblenz Jonathan Aldrich Brad A. Myers and Joshua Sunshine. 2020. Can advanced type systems be usable? An empirical study of ownership assets and typestate in Obsidian. OOPSLA.","DOI":"10.1145\/3428200"},{"key":"e_1_3_2_1_16_1","unstructured":"CompCert. 2023. CompCert. https:\/\/github.com\/AbsInt\/CompCert [Online] [Accessed: 2023-04-20]"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"e_1_3_2_1_18_1","first-page":"8","article-title":"The Coq Development Team. 2017","year":"2023","unstructured":"coq. 2023. The Coq Development Team. 2017. Coq, v.8.7.. https:\/\/coq.inria.fr [Online], [Accessed: 2023-04-20]","journal-title":"Coq"},{"key":"e_1_3_2_1_19_1","volume-title":"Improving the Stability of Type Safety Proofs in Dafny. In Dafny Workshop at POPL.","author":"Cutler Joseph W.","year":"2024","unstructured":"Joseph W. Cutler, Michael Hicks, and Emina Torlak. 2024. Improving the Stability of Type Safety Proofs in Dafny. In Dafny Workshop at POPL."},{"key":"e_1_3_2_1_20_1","unstructured":"Dafny. 2023. dafny-lang. https:\/\/github.com\/dafny-lang\/dafny [Online] [Accessed: 2023-04-20]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_22_1","volume-title":"Colouring Flags with Dafny & Idris. In Dafny Workshop at POPL.","author":"de Muijnck-Hughes Jan","year":"2024","unstructured":"Jan de Muijnck-Hughes and James Noble. 2024. Colouring Flags with Dafny & Idris. In Dafny Workshop at POPL."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421477"},{"key":"e_1_3_2_1_24_1","volume-title":"Robert Bruce Findler, and Matthew Flatt","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex (1st ed.). The MIT Press. isbn:0262062755"},{"volume-title":"Abstractions to Control the Future. Ph. D. Dissertation","author":"Fernandez-Reyes Kiko","key":"e_1_3_2_1_25_1","unstructured":"Kiko Fernandez-Reyes. 2021. Abstractions to Control the Future. Ph. D. Dissertation. Uppsala University."},{"key":"e_1_3_2_1_26_1","volume-title":"Dalarna: A Capability-Based Dynamic Language Design For Data Race Freedom. In FTfJP.","author":"Fernandez-Reyes Kiko","year":"2020","unstructured":"Kiko Fernandez-Reyes, James Noble, and Tobias Wrigstad. 2020. Dalarna: A Capability-Based Dynamic Language Design For Data Race Freedom. In FTfJP."},{"key":"e_1_3_2_1_27_1","volume-title":"Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom. In Submitted.","author":"Fernandez-Reyes Kiko","year":"2021","unstructured":"Kiko Fernandez-Reyes, James Noble, and Tobias Wrigstad. 2021. Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom. In Submitted."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Donald Gordon and James Noble. 2007. Dynamic Ownership in a Dynamic Language. In DLS.","DOI":"10.1145\/1297081.1297090"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.90445"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_31_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914, Broomfield, CO, USA, October 6-8, 2014, Jason Flinn and Hank Levy (Eds.). USENIX Association, 165\u2013181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"e_1_3_2_1_34_1","unstructured":"Vivian Hu. 2020. Rust Breaks into TIOBE Top 20 Most Popular Programming Languages. June InfoQ"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2020. Safe Systems Programming in Rust: The Promise and the Challenge. Communications of the ACM.","DOI":"10.1145\/3418295"},{"key":"e_1_3_2_1_36_1","volume-title":"The Rust Programming Language","author":"Klabnik Steve","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language (2nd ed.).","edition":"2"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_38_1","unstructured":"Paul Krill. 2021. Microsoft forms Rust language team. Feb. InfoWorld"},{"key":"e_1_3_2_1_39_1","first-page":"407","article-title":"The Boogie verification debugger. SEFM","volume":"7041","author":"Goues Claire Le","year":"2011","unstructured":"Claire Le Goues, K Rustan M Leino, and Micha\u0142 Moskal. 2011. The Boogie verification debugger. SEFM, LNCS, 7041 (2011), 407\u2013414.","journal-title":"LNCS"},{"key":"e_1_3_2_1_40_1","unstructured":"G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. R. Cok P. M\u00fcller J. Kiniry and P. Chalin. 2007. JML Reference Manual. February Iowa State Univ. \u00a7mall www.jmlspecs.org"},{"volume-title":"Object-Oriented Programming in the BETA Programming Language","author":"Madsen Ole Lehrmann","key":"e_1_3_2_1_41_1","unstructured":"Ole Lehrmann Madsen, Birger M\u00f8ller-Pedersen, and Kristen Nygaard. 1993. Object-Oriented Programming in the BETA Programming Language. Addison-Wesley."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606754"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_2_1_44_1","unstructured":"K. Rustan M. Leino. 2023. Program Proofs. MIT Press."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_46_1","unstructured":"Mikael Mayer. 2023. How to use Dafny to prove type safety. In Dafny Blog. dafny.org\/blog\/2023\/07\/14\/types-and-programming-languages"},{"key":"e_1_3_2_1_47_1","volume-title":"Enhancing Proof Stability. In Dafny Workshop at POPL.","author":"McLaughlin Sean","year":"2024","unstructured":"Sean McLaughlin, Georges-Axel Jaloyan, Tongtong Xiang, and Florian Rabe. 2024. Enhancing Proof Stability. In Dafny Workshop at POPL."},{"key":"e_1_3_2_1_48_1","unstructured":"Microsoft. 2023. The Dafny Programming and Verification Language. https:\/\/dafny.org\/ [Online] [Accessed: 2023-04-20]"},{"key":"e_1_3_2_1_49_1","unstructured":"Microsoft. 2023. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/ [Online] [Accessed: 2023-04-20]"},{"key":"e_1_3_2_1_50_1","volume-title":"Dafny. In Dafny Workshop at POPL.","author":"Noble James","year":"2024","unstructured":"James Noble. 2024. Learn \u2019em Dafny. In Dafny Workshop at POPL."},{"key":"e_1_3_2_1_51_1","unstructured":"James Noble David Clarke and John Potter. 1999. Object Ownership for Dynamic Alias Protection. In TOOLS."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_23"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"crossref","unstructured":"James Noble Jan Vitek and John Potter. 1998. Flexible Alias Protection. In ECOOP. 158\u2013185.","DOI":"10.1007\/BFb0054091"},{"key":"e_1_3_2_1_54_1","unstructured":"James Noble and Charles Weir. 2024. The Faultless Way of Programming: Principles Patterns Practices and Peculiarities for Verification in Dafny. In EuroPLoP."},{"key":"e_1_3_2_1_55_1","unstructured":"Matthew Parkinson. 2007. Class Invariants: the end of the Road? In IWACO."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"crossref","unstructured":"Boqin Qin Yilun Chen Zeming Yu Linhai Song and Yiying Zhang. 2020. Understanding memory and thread safety practices and issues in real-world Rust programs. In PLDI. 763\u2013779.","DOI":"10.1145\/zenodo.3756301"},{"key":"e_1_3_2_1_57_1","unstructured":"Walter Chalmers Smith. 1867. Immortal Invisible."},{"key":"e_1_3_2_1_58_1","unstructured":"Ryan James Spencer. 2020. Four Ways To Avoid The Wrath Of The Borrow Checker. justanotherdot.com"},{"key":"e_1_3_2_1_59_1","unstructured":"Zhenkun Yang Wen Wang Jeremy Casas Pasquale Cocchini and Jin Yang. 2023. Towards A Correct-by-Construction FHE Model. IACR Cryptol. ePrint Arch. 281."}],"event":{"name":"FTfJP '24: 26th ACM International Workshop on Formal Techniques for Java-like Programs","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"],"location":"Vienna Austria","acronym":"FTfJP '24"},"container-title":["Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678721.3686228","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:09:56Z","timestamp":1750295396000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678721.3686228"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,20]]},"references-count":59,"alternative-id":["10.1145\/3678721.3686228","10.1145\/3678721"],"URL":"https:\/\/doi.org\/10.1145\/3678721.3686228","relation":{},"subject":[],"published":{"date-parts":[[2024,9,20]]},"assertion":[{"value":"2024-09-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}