{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:10Z","timestamp":1780994710786,"version":"3.54.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We apply program verification technology to the problem of specifying and\nverifying automatic differentiation (AD) algorithms. We focus on define-by-run,\na style of AD where the program that must be differentiated is executed and\nmonitored by the automatic differentiation algorithm. We begin by asking, \"what\nis an implementation of AD?\" and \"what does it mean for an implementation of AD\nto be correct?\" We answer these questions both at an informal level, in precise\nEnglish prose, and at a formal level, using types and logical assertions. After\nanswering these broad questions, we focus on a specific implementation of AD,\nwhich involves a number of subtle programming-language features, including\ndynamically allocated mutable state, first-class functions, and effect\nhandlers. We present a machine-checked proof, expressed in a modern variant of\nSeparation Logic, of its correctness. We view this result as an advanced\nexercise in program verification, with potential future applications to the\nverification of more realistic automatic differentiation systems and of other\nsoftware components that exploit delimited-control effects.<\/jats:p>","DOI":"10.46298\/lmcs-19(4:5)2023","type":"journal-article","created":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T08:50:09Z","timestamp":1698051009000},"source":"Crossref","is-referenced-by-count":3,"title":["Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library"],"prefix":"10.46298","volume":"Volume 19, Issue 4","author":[{"given":"Paulo Em\u00edlio","family":"de Vilhena","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2023,10,23]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/lmcs.episciences.org\/12455\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/lmcs.episciences.org\/12455\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T08:50:09Z","timestamp":1698051009000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/8851"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(4:5)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2112.07292v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2112.07292v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2112.07292v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2112.07292","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2112.07292","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,23]]},"article-number":"8851"}}