{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:56:30Z","timestamp":1787064990772,"version":"3.56.0"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,1,11]],"date-time":"2022-01-11T00:00:00Z","timestamp":1641859200000},"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":[[2022,1,17]]},"DOI":"10.1145\/3497775.3503677","type":"proceedings-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:20:48Z","timestamp":1641946848000},"page":"82-99","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Specification and verification of a transient stack"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2169-1977","authenticated-orcid":false,"given":"Alexandre","family":"Moine","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arthur","family":"Chargu\u00e9raud","sequence":"additional","affiliation":[{"name":"Inria, France \/ University of Strasbourg, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44777-2_3"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"e_1_3_2_1_4_1","volume-title":"Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7, 2:17","author":"Atkey Robert","year":"2011","unstructured":"Robert Atkey . 2011. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7, 2:17 ( 2011 ), http:\/\/bentnib.org\/amortised-sep-logic-journal.pdf Robert Atkey. 2011. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7, 2:17 (2011), http:\/\/bentnib.org\/amortised-sep-logic-journal.pdf"},{"key":"e_1_3_2_1_5_1","unstructured":"Phil Bagwell. 2001. Ideal Hash Trees. EPFL. https:\/\/lampwww.epfl.ch\/papers\/idealhashtrees.pdf Phil Bagwell. 2001. Ideal Hash Trees. EPFL. https:\/\/lampwww.epfl.ch\/papers\/idealhashtrees.pdf"},{"key":"e_1_3_2_1_6_1","volume-title":"Rob DeLine, and Bart Jacobs.","author":"Barnett Mike","year":"2005","unstructured":"Mike Barnett , Bor-Yuh Evan Chang , Rob DeLine, and Bart Jacobs. 2005 . Boogie : A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects. Springer . https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2005\/01\/krml160.pdf Mike Barnett, Bor-Yuh Evan Chang, Rob DeLine, and Bart Jacobs. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects. Springer. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2005\/01\/krml160.pdf"},{"key":"e_1_3_2_1_7_1","unstructured":"Jean-Philippe Bernardy. 2021. The Haskell yi package. http:\/\/hackage.haskell.org\/package\/yi-0.6.2.3\/docs\/src\/Data-Rope.html Jean-Philippe Bernardy. 2021. The Haskell yi package. http:\/\/hackage.haskell.org\/package\/yi-0.6.2.3\/docs\/src\/Data-Rope.html"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the ACM on Programming Languages, 1, ICFP","author":"Bol\u00edvar Puente Juan Pedro","year":"2017","unstructured":"Juan Pedro Bol\u00edvar Puente . 2017 . Persistence for the masses: RRB-vectors in a systems language . Proceedings of the ACM on Programming Languages, 1, ICFP (2017), 16:1\u201316:28. https:\/\/public.sinusoid.es\/misc\/immer\/immer-icfp17.pdf Juan Pedro Bol\u00edvar Puente. 2017. Persistence for the masses: RRB-vectors in a systems language. Proceedings of the ACM on Programming Languages, 1, ICFP (2017), 16:1\u201316:28. https:\/\/public.sinusoid.es\/misc\/immer\/immer-icfp17.pdf"},{"key":"e_1_3_2_1_9_1","unstructured":"Lee Byron. 2021. Immutable.js library for JavaScript. https:\/\/github.com\/immutable-js\/immutable-js\/ Lee Byron. 2021. Immutable.js library for JavaScript. https:\/\/github.com\/immutable-js\/immutable-js\/"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_2_1_11_1","volume-title":"Program Verification Through Characteristic Formulae. In International Conference on Functional Programming (ICFP). 321\u2013332","author":"Chargu\u00e9raud Arthur","year":"2010","unstructured":"Arthur Chargu\u00e9raud . 2010 . Program Verification Through Characteristic Formulae. In International Conference on Functional Programming (ICFP). 321\u2013332 . http:\/\/www.chargueraud.org\/research\/2010\/cfml\/main.pdf Arthur Chargu\u00e9raud. 2010. Program Verification Through Characteristic Formulae. In International Conference on Functional Programming (ICFP). 321\u2013332. http:\/\/www.chargueraud.org\/research\/2010\/cfml\/main.pdf"},{"key":"e_1_3_2_1_12_1","volume-title":"Characteristic Formulae for the Verification of Imperative Programs. In International Conference on Functional Programming (ICFP). 418\u2013430","author":"Chargu\u00e9raud Arthur","year":"2011","unstructured":"Arthur Chargu\u00e9raud . 2011 . Characteristic Formulae for the Verification of Imperative Programs. In International Conference on Functional Programming (ICFP). 418\u2013430 . http:\/\/www.chargueraud.org\/research\/2011\/cfml\/main.pdf Arthur Chargu\u00e9raud. 2011. Characteristic Formulae for the Verification of Imperative Programs. In International Conference on Functional Programming (ICFP). 418\u2013430. http:\/\/www.chargueraud.org\/research\/2011\/cfml\/main.pdf"},{"key":"e_1_3_2_1_13_1","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2021. Sek. https:\/\/gitlab.inria.fr\/fpottier\/sek\/ Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2021. Sek. https:\/\/gitlab.inria.fr\/fpottier\/sek\/"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Arthur Chargu\u00e9raud. 2016. Higher-order representation predicates in separation logic. In Certified Programs and Proofs (CPP). 3\u201314. https:\/\/hal.inria.fr\/hal-01408670 Arthur Chargu\u00e9raud. 2016. Higher-order representation predicates in separation logic. In Certified Programs and Proofs (CPP). 3\u201314. https:\/\/hal.inria.fr\/hal-01408670","DOI":"10.1145\/2854065.2854068"},{"key":"e_1_3_2_1_15_1","unstructured":"Arthur Chargu\u00e9raud. 2021. The CFML tool and library. http:\/\/www.chargueraud.org\/softs\/cfml\/ Arthur Chargu\u00e9raud. 2021. The CFML tool and library. http:\/\/www.chargueraud.org\/softs\/cfml\/"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In Programming Language Design and Implementation (PLDI). 234\u2013245. http:\/\/adam.chlipala.net\/papers\/BedrockPLDI11\/BedrockPLDI11.pdf Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In Programming Language Design and Implementation (PLDI). 234\u2013245. http:\/\/adam.chlipala.net\/papers\/BedrockPLDI11\/BedrockPLDI11.pdf","DOI":"10.1145\/1993316.1993526"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_1_21_1","volume-title":"Semi-persistent Data Structures. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"336","author":"Conchon Sylvain","year":"2008","unstructured":"Sylvain Conchon and Jean-Christophe Filli\u00e2tre . 2008 . Semi-persistent Data Structures. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science , Vol. 4960). Springer, 322\u2013 336 . https:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/spds-esop08.pdf Sylvain Conchon and Jean-Christophe Filli\u00e2tre. 2008. Semi-persistent Data Structures. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 4960). Springer, 322\u2013336. https:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/spds-esop08.pdf"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Principles of Programming Languages (POPL). http:\/\/www.cse.chalmers.se\/~nad\/publications\/danielsson-popl2008.pdf Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Principles of Programming Languages (POPL). http:\/\/www.cse.chalmers.se\/~nad\/publications\/danielsson-popl2008.pdf","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90034-2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_24"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803395"},{"key":"e_1_3_2_1_29_1","unstructured":"Tobias Gustafsson. 2021. Pyrsistent library for Python. https:\/\/github.com\/tobgu\/pyrsistent Tobias Gustafsson. 2021. Pyrsistent library for Python. https:\/\/github.com\/tobgu\/pyrsistent"},{"key":"e_1_3_2_1_31_1","volume-title":"Interactive Theorem Proving (ITP) (Leibniz International Proceedings in Informatics","volume":"20","author":"Gu\u00e9neau Arma\u00ebl","year":"2019","unstructured":"Arma\u00ebl Gu\u00e9neau , Jacques-Henri Jourdan , Arthur Chargu\u00e9raud , and Fran\u00e7ois Pottier . 2019 . Formal Proof and Analysis of an Incremental Cycle Detection Algorithm . In Interactive Theorem Proving (ITP) (Leibniz International Proceedings in Informatics , Vol. 141). 18:1\u201318: 20 . http:\/\/gallium.inria.fr\/~fpottier\/publis\/gueneau-jourdan-chargueraud-pottier-2019.pdf Arma\u00ebl Gu\u00e9neau, Jacques-Henri Jourdan, Arthur Chargu\u00e9raud, and Fran\u00e7ois Pottier. 2019. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In Interactive Theorem Proving (ITP) (Leibniz International Proceedings in Informatics, Vol. 141). 18:1\u201318:20. http:\/\/gallium.inria.fr\/~fpottier\/publis\/gueneau-jourdan-chargueraud-pottier-2019.pdf"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2009.8.4.a3"},{"key":"e_1_3_2_1_33_1","volume-title":"European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"319","author":"Maximilian P.","unstructured":"Maximilian P. L. Haslbeck and Peter Lammich. 2021. For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM . In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science , Vol. 12648). Springer, 292\u2013 319 . https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich_LLVM_with_Time.pdf Maximilian P. L. Haslbeck and Peter Lammich. 2021. For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 12648). Springer, 292\u2013319. https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich_LLVM_with_Time.pdf"},{"key":"e_1_3_2_1_34_1","volume-title":"Haslbeck and Tobias Nipkow","author":"Maximilian P.","year":"2018","unstructured":"Maximilian P. L. Haslbeck and Tobias Nipkow . 2018 . Hoare Logics for Time Bounds: A Study in Meta Theory. In Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science , Vol. 10805). Springer, 155\u2013 171 . https:\/\/www21.in.tum.de\/~nipkow\/pubs\/tacas18.pdf Maximilian P. L. Haslbeck and Tobias Nipkow. 2018. Hoare Logics for Time Bounds: A Study in Meta Theory. In Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 10805). Springer, 155\u2013171. https:\/\/www21.in.tum.de\/~nipkow\/pubs\/tacas18.pdf"},{"key":"e_1_3_2_1_35_1","unstructured":"Rich Hickey. 2006. The Clojure programming language. https:\/\/clojure.org\/ Rich Hickey. 2006. The Clojure programming language. https:\/\/clojure.org\/"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005769"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL). 359\u2013373. http:\/\/www.cs.cmu.edu\/~janh\/papers\/HoffmannDW17.pdf Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL). 359\u2013373. http:\/\/www.cs.cmu.edu\/~janh\/papers\/HoffmannDW17.pdf","DOI":"10.1145\/3093333.3009842"},{"key":"e_1_3_2_1_38_1","unstructured":"Bart Jacobs and Frank Piessens. 2008. The VeriFast Program Verifier. Department of Computer Science Katholieke Universiteit Leuven. http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/verifast.pdf Bart Jacobs and Frank Piessens. 2008. The VeriFast Program Verifier. Department of Computer Science Katholieke Universiteit Leuven. http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/verifast.pdf"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237865"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Neelakantan R. Krishnaswami Jonathan Aldrich Lars Birkedal Kasper Svendsen and Alexandre Buisse. 2009. Design Patterns in Separation Logic. In Types in Language Design and Implementation (TLDI). 105\u2013116. http:\/\/www.cs.cmu.edu\/~neelk\/design-patterns-tldi09.pdf Neelakantan R. Krishnaswami Jonathan Aldrich Lars Birkedal Kasper Svendsen and Alexandre Buisse. 2009. Design Patterns in Separation Logic. In Types in Language Design and Implementation (TLDI). 105\u2013116. http:\/\/www.cs.cmu.edu\/~neelk\/design-patterns-tldi09.pdf","DOI":"10.1145\/1481861.1481874"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Peter Lammich. 2016. Refinement Based Verification of Imperative Data Structures. In Certified Programs and Proofs (CPP). 27\u201336. https:\/\/www21.in.tum.de\/~lammich\/pub\/cpp2016_impds.pdf Peter Lammich. 2016. Refinement Based Verification of Imperative Data Structures. In Certified Programs and Proofs (CPP). 27\u201336. https:\/\/www21.in.tum.de\/~lammich\/pub\/cpp2016_impds.pdf","DOI":"10.1145\/2854065.2854067"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9437-1"},{"key":"e_1_3_2_1_44_1","volume-title":"Efficient Verified Implementation of Introsort and Pdqsort","author":"Lammich Peter","unstructured":"Peter Lammich . 2020. Efficient Verified Implementation of Introsort and Pdqsort . In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing , Cham . 307\u2013323. isbn:978-3-030-51054-1 Peter Lammich. 2020. Efficient Verified Implementation of Introsort and Pdqsort. In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham. 307\u2013323. isbn:978-3-030-51054-1"},{"key":"e_1_3_2_1_45_1","unstructured":"Peter Lammich and Rene Meis. 2012. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs http:\/\/afp.sourceforge.net\/entries\/Separation_Logic_Imperative_HOL.shtml Peter Lammich and Rene Meis. 2012. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs http:\/\/afp.sourceforge.net\/entries\/Separation_Logic_Imperative_HOL.shtml"},{"key":"e_1_3_2_1_46_1","volume-title":"Improving RRB-Tree Performance through Transience. Master\u2019s thesis. Department of Computer and Information Science","author":"L\u2019Orange Jean Niklas","unstructured":"Jean Niklas L\u2019Orange . 2014. Improving RRB-Tree Performance through Transience. Master\u2019s thesis. Department of Computer and Information Science , Norwegian University of Science and Technology . https:\/\/hypirion.com\/thesis.pdf Jean Niklas L\u2019Orange. 2014. Improving RRB-Tree Performance through Transience. Master\u2019s thesis. Department of Computer and Information Science, Norwegian University of Science and Technology. https:\/\/hypirion.com\/thesis.pdf"},{"key":"e_1_3_2_1_47_1","volume-title":"Tools and Experiments (Lecture Notes in Computer Science","volume":"195","author":"Mehnert Hannes","year":"2012","unstructured":"Hannes Mehnert , Filip Sieczkowski , Lars Birkedal , and Peter Sestoft . 2012 . Formalized Verification of Snapshotable Trees: Separation and Sharing. In Verified Software: Theories , Tools and Experiments (Lecture Notes in Computer Science , Vol. 7152). Springer, 179\u2013 195 . https:\/\/cs.au.dk\/~birke\/papers\/snapshots-conf.pdf Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and Peter Sestoft. 2012. Formalized Verification of Snapshotable Trees: Separation and Sharing. In Verified Software: Theories, Tools and Experiments (Lecture Notes in Computer Science, Vol. 7152). Springer, 179\u2013195. https:\/\/cs.au.dk\/~birke\/papers\/snapshots-conf.pdf"},{"key":"e_1_3_2_1_48_1","volume-title":"Wei Xiang Leow, and Aquinas Hobor","author":"Mohan Anshuman","year":"2021","unstructured":"Anshuman Mohan , Wei Xiang Leow, and Aquinas Hobor . 2021 . Functional Correctness of C Implementations of Dijkstra\u2019s, Kruskal\u2019s , and Prim\u2019s Algorithms. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science , Vol. 12760). Springer, 801\u2013 826 . https:\/\/www.cs.cornell.edu\/~amohan\/papers\/dpk-as-published.pdf Anshuman Mohan, Wei Xiang Leow, and Aquinas Hobor. 2021. Functional Correctness of C Implementations of Dijkstra\u2019s, Kruskal\u2019s, and Prim\u2019s Algorithms. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 12760). Springer, 801\u2013826. https:\/\/www.cs.cornell.edu\/~amohan\/papers\/dpk-as-published.pdf"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Alexandre Moine Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2021. Specification and verification of a transient stack: source code and proofs. https:\/\/gitlab.inria.fr\/amoine\/cfml-sek Alexandre Moine Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2021. Specification and verification of a transient stack: source code and proofs. https:\/\/gitlab.inria.fr\/amoine\/cfml-sek","DOI":"10.1145\/3497775.3503677"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477355.3477362"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_21"},{"key":"e_1_3_2_1_54_1","unstructured":"Tobias Nipkow Jasmin Blanchette Manuel Eberl Alejandro G\u00f3mez-Londo\u00f1o Peter Lammich Christian Sternagel Simon Wimmer and Bohua Zhan. 2021. Functional Algorithms Verified!. https:\/\/functional-algorithms-verified.org Tobias Nipkow Jasmin Blanchette Manuel Eberl Alejandro G\u00f3mez-Londo\u00f1o Peter Lammich Christian Sternagel Simon Wimmer and Bohua Zhan. 2021. Functional Algorithms Verified!. https:\/\/functional-algorithms-verified.org"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9459-3"},{"key":"e_1_3_2_1_56_1","volume-title":"Haslbeck","author":"Nipkow Tobias","year":"2020","unstructured":"Tobias Nipkow , Manuel Eberl , and Maximilian P. L . Haslbeck . 2020 . Verified Textbook Algorithms: a Biased Survey. In Automated Technology for Verification and Analysis (ATVA) (Lecture Notes in Computer Science , Vol. 12302). Springer, 25\u2013 53 . https:\/\/www21.in.tum.de\/~nipkow\/pubs\/atva20.pdf Tobias Nipkow, Manuel Eberl, and Maximilian P. L. Haslbeck. 2020. Verified Textbook Algorithms: a Biased Survey. In Automated Technology for Verification and Analysis (ATVA) (Lecture Notes in Computer Science, Vol. 12302). Springer, 25\u201353. https:\/\/www21.in.tum.de\/~nipkow\/pubs\/atva20.pdf"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_2_1_58_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","unstructured":"Chris Okasaki . 1999. Purely Functional Data Structures . Cambridge University Press . http:\/\/www.cambridge.org\/us\/catalogue\/catalogue.asp?isbn=0521663504 Chris Okasaki. 1999. Purely Functional Data Structures. Cambridge University Press. http:\/\/www.cambridge.org\/us\/catalogue\/catalogue.asp?isbn=0521663504"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Alexandre Pilkiewicz and Fran\u00e7ois Pottier. 2011. The essence of monotonic state. In Types in Language Design and Implementation (TLDI). http:\/\/gallium.inria.fr\/~fpottier\/publis\/pilkiewicz-pottier-monotonicity.pdf Alexandre Pilkiewicz and Fran\u00e7ois Pottier. 2011. The essence of monotonic state. In Types in Language Design and Implementation (TLDI). http:\/\/gallium.inria.fr\/~fpottier\/publis\/pilkiewicz-pottier-monotonicity.pdf","DOI":"10.1145\/1929553.1929565"},{"key":"e_1_3_2_1_60_1","volume-title":"Furia","author":"Polikarpova Nadia","year":"2015","unstructured":"Nadia Polikarpova , Julian Tschannen , and Carlo A . Furia . 2015 . A Fully Verified Container Library . In Formal Methods (FM) (Lecture Notes in Computer Science, Vol. 9109). Springer, 414\u2013 434 . http:\/\/se.inf.ethz.ch\/people\/tschannen\/publications\/ptf-fm15.pdf Nadia Polikarpova, Julian Tschannen, and Carlo A. Furia. 2015. A Fully Verified Container Library. In Formal Methods (FM) (Lecture Notes in Computer Science, Vol. 9109). Springer, 414\u2013434. http:\/\/se.inf.ethz.ch\/people\/tschannen\/publications\/ptf-fm15.pdf"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Pottier. 2008. Hiding local state in direct style: a higher-order anti-frame rule. In Logic in Computer Science (LICS). 331\u2013340. http:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier-antiframe-2008.pdf Fran\u00e7ois Pottier. 2008. Hiding local state in direct style: a higher-order anti-frame rule. In Logic in Computer Science (LICS). 331\u2013340. http:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier-antiframe-2008.pdf","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Pottier. 2017. Verifying a hash table and its iterators in higher-order separation logic. In Certified Programs and Proofs (CPP). 3\u201316. http:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier-hashtable.pdf Fran\u00e7ois Pottier. 2017. Verifying a hash table and its iterators in higher-order separation logic. In Certified Programs and Proofs (CPP). 3\u201316. http:\/\/gallium.inria.fr\/~fpottier\/publis\/fpottier-hashtable.pdf","DOI":"10.1145\/3018610.3018624"},{"key":"e_1_3_2_1_63_1","unstructured":"Tristan Ravitch. 2020. Persistent Vector library for Haskell. https:\/\/github.com\/travitch\/persistent-vector Tristan Ravitch. 2020. Persistent Vector library for Haskell. https:\/\/github.com\/travitch\/persistent-vector"},{"key":"e_1_3_2_1_64_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). 55\u201374","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). 55\u201374 . http:\/\/www.cs.cmu.edu\/~jcr\/seplogic.pdf John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). 55\u201374. http:\/\/www.cs.cmu.edu\/~jcr\/seplogic.pdf"},{"key":"e_1_3_2_1_65_1","volume-title":"Program-ing Finger Trees in Coq. In International Conference on Functional Programming (ICFP). 13\u201324","author":"Sozeau Matthieu","year":"2007","unstructured":"Matthieu Sozeau . 2007 . Program-ing Finger Trees in Coq. In International Conference on Functional Programming (ICFP). 13\u201324 . http:\/\/mattam.org\/research\/publications\/Program-ing_Finger_Trees_in_Coq.pdf Matthieu Sozeau. 2007. Program-ing Finger Trees in Coq. In International Conference on Functional Programming (ICFP). 13\u201324. http:\/\/mattam.org\/research\/publications\/Program-ing_Finger_Trees_in_Coq.pdf"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784739"},{"key":"e_1_3_2_1_67_1","volume-title":"Jean Karim Zinzindohoue, and Santiago Zanella B\u00e9guelin","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy , Catalin Hritcu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , Simon Forest , Karthikeyan Bhargavan , C\u00e9dric Fournet , Pierre-Yves Strub , Markulf Kohlweiss , Jean Karim Zinzindohoue, and Santiago Zanella B\u00e9guelin . 2016 . Dependent types and multi-monadic effects in F^\u22c6. In Principles of Programming Languages (POPL) . 256\u2013270. https:\/\/www.fstar-lang.org\/papers\/mumon\/ Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella B\u00e9guelin. 2016. Dependent types and multi-monadic effects in F^\u22c6. In Principles of Programming Languages (POPL). 256\u2013270. https:\/\/www.fstar-lang.org\/papers\/mumon\/"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"crossref","unstructured":"Amin Timany and Lars Birkedal. 2021. Reasoning about monotonicity in separation logic. In Certified Programs and Proofs (CPP). 91\u2013104. https:\/\/iris-project.org\/pdfs\/2021-CPP-monotone-final.pdf Amin Timany and Lars Birkedal. 2021. Reasoning about monotonicity in separation logic. In Certified Programs and Proofs (CPP). 91\u2013104. https:\/\/iris-project.org\/pdfs\/2021-CPP-monotone-final.pdf","DOI":"10.1145\/3437992.3439931"}],"event":{"name":"CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Philadelphia PA USA","acronym":"CPP '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503677","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3497775.3503677","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:49:25Z","timestamp":1750178965000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503677"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,11]]},"references-count":68,"alternative-id":["10.1145\/3497775.3503677","10.1145\/3497775"],"URL":"https:\/\/doi.org\/10.1145\/3497775.3503677","relation":{},"subject":[],"published":{"date-parts":[[2022,1,11]]},"assertion":[{"value":"2022-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}