{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:11:36Z","timestamp":1760033496497,"version":"build-2065373602"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100020884","name":"Agencia Nacional de Investigaci\u00f3n y Desarrollo","doi-asserted-by":"publisher","award":["ANID\/Doctorado Nacional\/2022-21221100"],"award-info":[{"award-number":["ANID\/Doctorado Nacional\/2022-21221100"]}],"id":[{"id":"10.13039\/501100020884","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012950","name":"Institut national de recherche en informatique et en automatique","doi-asserted-by":"publisher","award":["GRAPA"],"award-info":[{"award-number":["GRAPA"]}],"id":[{"id":"10.13039\/100012950","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Certified programming, as carried out in proof assistants and dependently-typed programming languages, ensures that a software meets its requirements by supporting the definition of both specifications and proofs. However, proofs easily break with partial definitions and incremental changes because specifications are not designed to account for the intermediate incomplete states of programs. We advocate for proper support for incremental certified programming by analyzing its objectives and inherent challenges, and propose a formal framework for achieving incremental certified programming in a principled manner. The key idea is to define appropriate notions of completion refinement and completeness to capture incrementality, and to systematically produce specifications that are valid at every stage of development while preserving the intent of the original statements.  \nWe provide a prototype implementation in the Rocq Prover, called IncRease, which exploits typeclasses for automation and extensibility, and is independent of any specific mechanism used to handle incompleteness. We illustrate its use with both an incremental textbook formalization of the simply-typed \u03bb-calculus, and a more complex case study of incremental certified programming for an existing dead-code elimination optimization pass of the CompCert project. We show that the approach is compatible with randomized property-based testing as provided by QuickChick. Finally we study how to combine incremental certified programming with deductive synthesis, using a novel incrementality-friendly adaptation of the Fiat library. This work provides theoretical and practical foundations towards systematic support for incremental certified programming, highlighting challenges and perspectives for future developments.<\/jats:p>","DOI":"10.1145\/3763068","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"499-526","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Incremental Certified Programming"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4140-1351","authenticated-orcid":false,"given":"Tom\u00e1s","family":"D\u00edaz","sequence":"first","affiliation":[{"name":"University of Chile, Santiago, Chile"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-3203","authenticated-orcid":false,"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion58688.2023.00018"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276945.3276946"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434341"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_1_16_1","volume-title":"QuickChick: Property-Based Testing for Coq. In Coq Workshop.","author":"D\u00e9n\u00e8s Maxime","unstructured":"Maxime D\u00e9n\u00e8s, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. 2014. QuickChick: Property-Based Testing for Coq. In Coq Workshop."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434338"},{"key":"e_1_2_1_18_1","volume-title":"Operational Refinement for Compiler Correctness. Ph. D. Dissertation","author":"Dockins Robert W.","unstructured":"Robert W. Dockins. 2012. Operational Refinement for Compiler Correctness. Ph. D. Dissertation. Princeton University."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Tom\u00e1s D\u00edaz Kenji Maillard Nicolas Tabareau and \u00c9ric Tanter. 2025. Incremental Certified Programming. https:\/\/doi.org\/10.5281\/zenodo.16913455 Archived version of the submitted artifact 10.5281\/zenodo.16913455","DOI":"10.5281\/zenodo.16913455"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2017.21"},{"key":"e_1_2_1_22_1","volume-title":"Axiomatic domain theory in categories of partial maps. Ph. D. Dissertation","author":"Fiore Marcelo P.","year":"1842","unstructured":"Marcelo P. Fiore. 1994. Axiomatic domain theory in categories of partial maps. Ph. D. Dissertation. University of Edinburgh, UK. https:\/\/hdl.handle.net\/1842\/406"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373817"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Son Ho and Cl\u00e9ment Pit-Claudel. 2024. Incremental Proof Development in Dafny with Module-Based Induction. arXiv preprint arXiv:2401.16233 https:\/\/doi.org\/10.48550\/arXiv.2401.16233 10.48550\/arXiv.2401.16233","DOI":"10.48550\/arXiv.2401.16233"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377812.3382156"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591286"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3495528"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2024.26"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_2_1_36_1","volume-title":"Programming from specifications","author":"Morgan Carroll","unstructured":"Carroll Morgan. 1994. Programming from specifications, 2nd Edition. Prentice Hall, Oxford, United Kingdom. isbn:978-0-13-123274-7","edition":"2"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_9"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341712"},{"key":"e_1_2_1_43_1","unstructured":"Benjamin C. Pierce Chris Casinghino Marco Gaboardi Michael Greenberg C\u01cet\u01celin Hri\u0163cu Vilhelm Sjoberg and Brent Yorgey. 2015. Software Foundations. Electronic textbook. http:\/\/www.cis.upenn.edu\/ bcpierce\/sf"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704912"},{"key":"e_1_2_1_45_1","volume-title":"Information Processing 83","author":"Reynolds John C.","unstructured":"John C. Reynolds. 1983. Types, abstraction, and parametric polymorphism. In Information Processing 83, R. E. A. Mason (Ed.). Elsevier, 513\u2013523."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric Zachary Tatlock et al. 2019. QED at large: A survey of engineering of formally verified software. Foundations and Trends\u00ae in Programming Languages 5 2-3 (2019) 102\u2013281. https:\/\/doi.org\/10.1561\/2500000045 10.1561\/2500000045","DOI":"10.1561\/2500000045"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454033"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.26"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_1_51_1","volume-title":"The Fourth International Workshop on Coq for Programming Languages","author":"Tassi Enrico","year":"2018","unstructured":"Enrico Tassi. 2018. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi \u03bb Prolog dialect). In The Fourth International Workshop on Coq for Programming Languages. Los Angeles (CA), United States."},{"key":"e_1_2_1_52_1","unstructured":"The Rocq Development Team. 2024. The Rocq prover reference manual. https:\/\/rocq-prover.org\/refman Version 8.20"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563355"},{"key":"e_1_2_1_54_1","unstructured":"Philip Wadler. 1998. https:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/ expression.txt"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/362575.362577"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586048"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763068","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:45:09Z","timestamp":1760031909000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763068"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":58,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763068"],"URL":"https:\/\/doi.org\/10.1145\/3763068","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}