{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T02:37:16Z","timestamp":1777775836964,"version":"3.51.4"},"reference-count":581,"publisher":"Emerald","issue":"2-3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,9,3]]},"abstract":"<jats:p>Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been available for over 40 years, but have only recently seen wide practical use. Projects based on construction of machine-checked formal proofs are now reaching an unprecedented scale, comparable to large software projects, which leads to new challenges in proof development and maintenance. Despite its increasing importance, the field of proof engineering is seldom considered in its own right; related theories, techniques, and tools span many fields and venues. This survey of the literature presents a holistic understanding of proof engineering for program correctness, covering impact in practice, foundations, proof automation, proof organization, and practical proof development.<\/jats:p>","DOI":"10.1561\/2500000045","type":"journal-article","created":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T05:33:31Z","timestamp":1567488811000},"page":"102-281","source":"Crossref","is-referenced-by-count":39,"title":["QED at Large: A Survey of Engineering of Formally Verified Software"],"prefix":"10.1108","volume":"5","author":[{"given":"Talia","family":"Ringer","sequence":"first","affiliation":[{"name":"University of Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Palmskog","sequence":"additional","affiliation":[{"name":"University of Texas at Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"Yale-NUS College"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milos","family":"Gligoric","sequence":"additional","affiliation":[{"name":"University of Texas at Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","published-online":{"date-parts":[[2019,9,3]]},"reference":[{"key":"2026032910223726800_ref001","volume-title":"POPLMark Reloaded","author":"Abel","year":"2017"},{"key":"2026032910223726800_ref002","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110277","volume-title":"Normalization by Evaluation for Sized Dependent Types","author":"Abel","year":"2017"},{"key":"2026032910223726800_ref003","unstructured":"ACL2 Development Team\n          . 1990-2019. \u201cACL2\u201d. url: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2."},{"key":"2026032910223726800_ref004","unstructured":"ACM SIGPLAN\n          . 2016. \u201cMost Influential POPL Paper Award\u201d. url: http:\/\/www.sigplan.org\/Awards\/POPL."},{"key":"2026032910223726800_ref005","doi-asserted-by":"publisher","first-page":"5367","DOI":"10.1007\/978-3-662-49224-6_6","volume-title":"Software Engineering and Formal Methods","author":"Adams","year":"2015"},{"key":"2026032910223726800_ref006","unstructured":"Agda Development Team\n          . 2005-2017. \u201cQuick Guide to Editing, Type Checking and Compiling Agda Code - Agda 2.5.4.2 Documentation\u201d. url: http:\/\/agda.readthedocs.io\/en\/v2.5.4.2\/getting-started\/quick-guide.html#quick-guide-introduction"},{"key":"2026032910223726800_ref007","unstructured":"Agda Development Team\n          . 2005-2018. \u201cCubical Type Theory in Agda -Agda 2.6.0 Documentation\u201d. url: http:\/\/agda.readthedocs.io\/en\/latest\/language\/cubical.html."},{"key":"2026032910223726800_ref008","unstructured":"Agda Development Team\n          . 2007-2019. \u201cThe Agda Wiki\u201d. url: http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php."},{"issue":"2","key":"2026032910223726800_ref009","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1006\/jsco.1997.0175","article-title":"Interactive Theorem Proving: An Empirical Study of User Activity","volume":"25","author":"Aitken","year":"1998","journal-title":"Journal of Symbolic Computation"},{"issue":"6","key":"2026032910223726800_ref010","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/S0953-5438(99)00023-5","article-title":"An analysis of errors in interactive proof attempts","volume":"12","author":"Aitken","year":"2000","journal-title":"Interacting with Computers"},{"key":"2026032910223726800_ref011","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1411260.1411266","volume-title":"SASyLF: An Educational Proof Assistant for Language Theory","author":"Aldrich","year":"2008"},{"key":"2026032910223726800_ref012","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/LICS.1990.113737","volume-title":"The semantics of reflected proof","author":"Allen","year":"1990"},{"key":"2026032910223726800_ref013","unstructured":"Altenkirch, T., V.Gaspes, B.Nordstr\u00f6m, and B.von Sydow. 1994. \u201cA user\u2019s guide to ALF\u201d. url: http:\/\/www.cse.chalmers.se\/~bengt\/papers\/usersguidetoalf.pdf."},{"key":"2026032910223726800_ref014","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/2872362.2872404","volume-title":"Cogent: Verifying High-Assurance File System Implementations","author":"Amani","year":"2016"},{"key":"2026032910223726800_ref015","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-45685-6_3","volume-title":"Theorem Proving in Higher Order Logics","author":"Ambler","year":"2002"},{"key":"2026032910223726800_ref016","unstructured":"Notices of the American Mathematical Society\n          . 2008: A Special Issue on Formal Proof. url: http:\/\/www.ams.org\/notices\/200811\/."},{"key":"2026032910223726800_ref017","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/3009837.3009866","volume-title":"Type Soundness Proofs with Definitional Interpreters","author":"Amin","year":"2017"},{"key":"2026032910223726800_ref018","unstructured":"Anand, A., A. W.Appel, G.Morrisett, M.Weaver, M.Sozeau, O.Savary Belanger, R.Pollack, and Z.Paraskevopoulou. 2017. \u201cCertiCoq: A verified compiler for Coq\u201d. In: CoqPL. URL: http:\/\/www.cs.princeton.edu\/~appel\/papers\/certicoq-coqpl.pdf."},{"key":"2026032910223726800_ref019","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-94821-8_2","volume-title":"Interactive Theorem Proving","author":"Anand","year":"2018"},{"key":"2026032910223726800_ref020","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-08970-6_3","volume-title":"Interactive Theorem Proving","author":"Anand","year":"2014"},{"key":"2026032910223726800_ref021","volume-title":"Operating Systems: Principles and Practice","author":"Anderson","year":"2014"},{"key":"2026032910223726800_ref022","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1109\/ICSE.2012.6227120","volume-title":"Large-Scale Formal Verification in Practice: A Process Perspective","author":"Andronick","year":"2012"},{"key":"2026032910223726800_ref023","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.274.1","volume-title":"The RedPRL Proof Assistant (Invited Paper)","author":"Angiuli","year":"2018"},{"key":"2026032910223726800_ref024","unstructured":"Appel, A. W.\n          \n          2006. \u201cTactics for separation logic\u201d. INRIA Rocquen-court and Princeton University, Early Draft. URL: https:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf."},{"key":"2026032910223726800_ref025","volume-title":"Personal communication","author":"Appel","year":"2017"},{"key":"2026032910223726800_ref026","unstructured":"Appel, A. W.\n          \n          2011a. \u201cEfficient Verified Red-Black Trees\u201d. URL: https:\/\/www.cs.princeton.edu\/~appel\/papers\/redblack.pdf."},{"key":"2026032910223726800_ref027","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Verified Software Toolchain","author":"Appel","year":"2011"},{"key":"2026032910223726800_ref028","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"Appel","year":"2014"},{"issue":"3","key":"2026032910223726800_ref029","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1023\/B:JARS.0000021013.61329.58","article-title":"A Trustworthy Proof Checker","volume":"31","author":"Appel","year":"2003","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"2026032910223726800_ref030","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s10817-011-9226-1","article-title":"A list-machine benchmark for mechanized metatheory","volume":"49","author":"Appel","year":"2012","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref031","volume-title":"The Works of Aristotle","author":"Aristotle","year":"1926"},{"key":"2026032910223726800_ref032","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290384","volume-title":"ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS","author":"Armstrong","year":"2019"},{"issue":"2","key":"2026032910223726800_ref033","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","article-title":"User interaction with the Matita proof assistant","volume":"39","author":"Asperti","year":"2007","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref034","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11617990_2","volume-title":"A content based mathematical search engine: Whelp","author":"Asperti","year":"2004"},{"key":"2026032910223726800_ref035","unstructured":"Aspinall, D.\n          \n          2000a. \u201cIsamode\u201d. url: https:\/\/homepages.inf.ed.ac.uk\/da\/Isamode\/doc\/Isamode_toc.html."},{"key":"2026032910223726800_ref036","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Proof General: A Generic Tool for Proof Development","author":"Aspinall","year":"2000"},{"issue":"1","key":"2026032910223726800_ref037","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0304-3975(00)00175-4","article-title":"Subtyping dependent types","volume":"266","author":"Aspinall","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"2026032910223726800_ref038","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-662-49665-7_19","volume-title":"Fundamental Approaches to Software Engineering","author":"Aspinall","year":"2016"},{"key":"2026032910223726800_ref039","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-319-43144-4_28","volume-title":"Interactive Theorem Proving","author":"Aspinall","year":"2016"},{"key":"2026032910223726800_ref040","unstructured":"Avigad, J.\n          \n          2004. \u201cProof Mining\u201d. url: http:\/\/www.andrew.cmu.edu\/user\/avigad\/Talks\/asl04.pdf."},{"key":"2026032910223726800_ref041","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Mechanized Metatheory for the Masses: The POPLMark Challenge","author":"Aydemir","year":"2005"},{"key":"2026032910223726800_ref042","unstructured":"Aydemir, B. E., A.Bohannon, M.Fairbairn, J. N.Foster, B. C.Pierce, P.Sewell, D.Vytiniotis, G.Washburn, S.Weirich, and S.Zdancewic. 2005-2019. \u201cThe POPLMark Challenge\u201d. url: http:\/\/www.seas.upenn.edu\/~plclub\/poplmark\/."},{"key":"2026032910223726800_ref043","volume-title":"Nominal Reasoning Techniques in Coq","author":"Aydemir","year":"2006"},{"key":"2026032910223726800_ref044","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1328438.1328443","volume-title":"Engineering Formal Metatheory","author":"Aydemir","year":"2008"},{"key":"2026032910223726800_ref045","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-1-4471-3756-6_7","volume-title":"Refinement Diagrams","author":"Back","year":"1991"},{"issue":"6","key":"2026032910223726800_ref046","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","article-title":"A calculus of refinements for program derivations","volume":"25","author":"Back","year":"1988","journal-title":"Acta Informatica"},{"issue":"8","key":"2026032910223726800_ref047","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/359576.359579","article-title":"Can Programming Be Liberated from the von Neumann Style?: A Functional Style and Its Algebra of Programs","volume":"21","author":"Backus","year":"1978","journal-title":"Commun. ACM"},{"key":"2026032910223726800_ref048","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1017\/S0956796815000180","article-title":"Calculating correct compilers","volume-title":"J. Funct. Program","author":"Bahr","year":"2015"},{"key":"2026032910223726800_ref049","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11812289_4","volume-title":"Mathematical Knowledge Management","author":"Ballarin","year":"2006"},{"issue":"1","key":"2026032910223726800_ref050","doi-asserted-by":"crossref","first-page":"41","DOI":"10.2478\/forma-2013-0004","article-title":"The fundamental properties of natural numbers","volume":"1","author":"Bancerek","year":"1990","journal-title":"Formalized Mathematics"},{"key":"2026032910223726800_ref051","article-title":"HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)","volume-title":"CoRR","author":"Bansal","year":"2019"},{"key":"2026032910223726800_ref052","doi-asserted-by":"publisher","DOI":"10.1002\/9780470050118.ecse579","volume-title":"Wiley Encyclopedia of Computer Science and Engineering","author":"Barendregt","year":"2007"},{"key":"2026032910223726800_ref053","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-00966-7_1","volume-title":"Mathematics, Computer Science and Logic - A Never Ending Story: The Bruno Buchberger Festschrift","author":"Barendregt","year":"2013"},{"issue":"3","key":"2026032910223726800_ref054","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","article-title":"Autarkic Computations in Formal Proofs","volume":"28","author":"Barendregt","year":"2002","journal-title":"Journal of Automated Reasoning"},{"issue":"1835","key":"2026032910223726800_ref055","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","article-title":"The challenge of computer mathematics","volume":"363","author":"Barendregt","year":"2005","journal-title":"Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences"},{"issue":"1","key":"2026032910223726800_ref056","doi-asserted-by":"publisher","first-page":"29","DOI":"10.6092\/issn.1972-5787\/1695","article-title":"Sets in Coq, Coq in Sets","volume":"3","author":"Barras","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"2026032910223726800_ref057","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-39320-4_29","volume-title":"Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems","author":"Barras","year":"2013"},{"key":"2026032910223726800_ref058","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-22102-1_4","volume-title":"Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface","author":"Barras","year":"2015"},{"key":"2026032910223726800_ref059","unstructured":"Barras, B. and B.Werner. 1997. \u201cCoq in Coq\u201d. URL: http:\/\/www.lix.polytechnique.fr\/Labo\/Bruno.Barras\/publi\/coqincoq.pdf."},{"key":"2026032910223726800_ref060","unstructured":"Barret, C.\n          \n          2018. \u201cTwitter Response\u201d. uRL: http:\/\/twitter.com\/cbarrett\/status\/1059888137026068482."},{"key":"2026032910223726800_ref061","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61780-9_58","volume-title":"Implicit coercions in type systems","author":"Barthe","year":"1995"},{"key":"2026032910223726800_ref062","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45685-6_4","volume-title":"Efficient reasoning about executable specifications in Coq","author":"Barthe","year":"2002"},{"key":"2026032910223726800_ref063","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45315-6_4","volume-title":"Foundations of Software Science and Computation Structures","author":"Barthe","year":"2001"},{"key":"2026032910223726800_ref064","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-61780-9_59","volume-title":"A two-level approach towards lean proof-checking","author":"Barthe","year":"1996"},{"key":"2026032910223726800_ref065","volume-title":"A Logic for Correct Program Development","author":"Bates","year":"1979"},{"key":"2026032910223726800_ref066","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/3018610.3018615","volume-title":"The HoTT Library: A Formalization of Homotopy Type Theory in Coq","author":"Bauer","year":"2017"},{"key":"2026032910223726800_ref067","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-15201-1_1","volume-title":"A Usability Evaluation of Interactive Theorem Provers Using Focus Groups","author":"Beckert","year":"2014"},{"key":"2026032910223726800_ref068","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/S0049-237X(08)70222-2","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Benthem Jutting","year":"1994"},{"key":"2026032910223726800_ref069","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/s11225-006-6604-5","article-title":"Program extraction from normalization proofs","volume-title":"Studia Logica","author":"Berger","year":"2005"},{"key":"2026032910223726800_ref070","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Executing Higher Order Logic","author":"Berghofer","year":"2002"},{"issue":"5","key":"2026032910223726800_ref071","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2007.01.018","article-title":"A Head-to-Head Comparison of de Bruijn Indices and Names","volume":"174","author":"Berghofer","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2026032910223726800_ref072","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"Berghofer","year":"1999"},{"key":"2026032910223726800_ref073","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1017\/CBO9780511770524.016","volume-title":"From Semantics to Computer Science: Essays in Honour of Gilles Kahn","author":"Bertot","year":"2009"},{"key":"2026032910223726800_ref074","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science An EATCS Series","author":"Bertot","year":"2004"},{"key":"2026032910223726800_ref075","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-57887-0_94","volume-title":"Theoretical Aspects of Computer Software","author":"Bertot","year":"1994"},{"issue":"2","key":"2026032910223726800_ref076","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jsco.1997.0171","article-title":"A Generic Approach to Building User Interfaces for Theorem Provers","volume":"25","author":"Bertot","year":"1998","journal-title":"Journal of Symbolic Computation"},{"key":"2026032910223726800_ref077","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-66167-4_1","volume-title":"Frontiers of Combining Systems","author":"Biendarra","year":"2017"},{"key":"2026032910223726800_ref078","unstructured":"Birkedal, L. and A.Bizjak. 2018. \u201cLecture Notes on Iris: Higher-Order Concurrent Separation Logic\u201d. uRL: https:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf."},{"key":"2026032910223726800_ref079","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61667-9","volume-title":"Constructive Analysis","author":"Bishop","year":"1985"},{"issue":"1","key":"2026032910223726800_ref080","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3243650","article-title":"Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP\/IP and the Sockets API","volume":"66","author":"Bishop","year":"2018","journal-title":"J. ACM"},{"key":"2026032910223726800_ref081","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/1111037.1111043","volume-title":"Engineering with Logic: HOL Specification and Symbolic-evaluation Testing for TCP Implementations","author":"Bishop","year":"2006"},{"key":"2026032910223726800_ref082","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-06410-9_4","volume-title":"40 Years of Formal Methods","author":"Bj\u00f8rner","year":"2014"},{"key":"2026032910223726800_ref083","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"Blanchette","year":"2011"},{"issue":"1","key":"2026032910223726800_ref084","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/s10817-018-9455-7","article-title":"A verified SAT solver framework with learn, forget, restart, and incrementality","volume":"61","author":"Blanchette","year":"2018","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"2026032910223726800_ref085","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","article-title":"A Learning-Based Fact Selector for Isabelle\/HOL","volume":"57","author":"Blanchette","year":"2016","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref086","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-20615-8_1","volume-title":"Mining the Archive of Formal Proofs","author":"Blanchette","year":"2015"},{"issue":"1","key":"2026032910223726800_ref087","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","article-title":"Hammering towards QED","volume":"9","author":"Blanchette","year":"2016","journal-title":"Journal of Formalized Reasoning"},{"key":"2026032910223726800_ref088","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Nitpick: A Counterexample Generator for Higher-order Logic Based on a Relational Model Finder","author":"Blanchette","year":"2010"},{"key":"2026032910223726800_ref089","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-30142-4_4","volume-title":"Proof Reuse with Extended Inductive Types","author":"Boite","year":"2004"},{"key":"2026032910223726800_ref090","first-page":"129","volume-title":"Experience with Embedding Hardware Description Languages in HOL","author":"Boulton","year":"1992"},{"key":"2026032910223726800_ref091","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/3173574.3173805","volume-title":"Inferring Loop Invariants through Gamification","author":"Bounov","year":"2018"},{"key":"2026032910223726800_ref092","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31374-5_3","volume-title":"Challenges and Experiences in Managing Large-Scale Proofs","author":"Bourke","year":"2012"},{"key":"2026032910223726800_ref093","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Using reflection to build efficient and certified decision procedures","author":"Boutin","year":"1997"},{"key":"2026032910223726800_ref094","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/3-540-58156-1_17","volume-title":"A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?","author":"Boyer","year":"1994"},{"key":"2026032910223726800_ref095","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"Bradley","year":"2007"},{"issue":"5","key":"2026032910223726800_ref096","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","article-title":"Idris, a general-purpose dependently typed programming language: Design and implementation","volume":"23","author":"Brady","year":"2013","journal-title":"Journal of Functional Programming"},{"key":"2026032910223726800_ref097","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-25379-9_14","volume-title":"Tactics for Reasoning Modulo AC in Coq","author":"Braibant","year":"2011"},{"issue":"1","key":"2026032910223726800_ref098","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:16)2012","article-title":"Deciding Kleene Algebras in Coq","volume":"8","author":"Braibant","year":"2012","journal-title":"Logical Methods in Computer Science"},{"issue":"2","key":"2026032910223726800_ref099","first-page":"9","article-title":"Theory exploration with Theorema","volume":"38","author":"Buchberger","year":"2000","journal-title":"Analele Universitatii Din Timisoara, ser. Matematica-Informatica"},{"issue":"4","key":"2026032910223726800_ref100","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","article-title":"Theorema: Towards computer-aided mathematical theory exploration","volume":"4","author":"Buchberger","year":"2006","journal-title":"Journal of Applied Logic"},{"key":"2026032910223726800_ref101","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"The New Quickcheck for Isabelle: Random, Exhaustive and Symbolic Testing Under One Roof","author":"Bulwahn","year":"2012"},{"key":"2026032910223726800_ref102","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"The Use of Explicit Plans to Guide Inductive Proofs","author":"Bundy","year":"1988"},{"issue":"1","key":"2026032910223726800_ref103","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","article-title":"Proving Properties of Programs by Structural Induction","volume":"12","author":"Burstall","year":"1969","journal-title":"The Computer Journal"},{"key":"2026032910223726800_ref104","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-58450-1_37","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"Busch","year":"1994"},{"key":"2026032910223726800_ref105","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15260-3","volume-title":"Introduction to Reliable and Secure Distributed Programming","author":"Cachin","year":"2011","edition":"2nd"},{"issue":"1","key":"2026032910223726800_ref106","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1010648911114","article-title":"An implementation of LF with coercive subtyping & universes","volume":"27","author":"Callaghan","year":"2001","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref107","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2676724.2693162","volume-title":"Practical tactics for verifying C programs in Coq","author":"Cao","year":"2015"},{"issue":"1","key":"2026032910223726800_ref108","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","article-title":"VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs","volume":"61","author":"Cao","year":"2018","journal-title":"Journal of Automated Reasoning"},{"issue":"SI","key":"2026032910223726800_ref109","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/223427.211821","article-title":"A Logical Framework for Software Proof Reuse","volume":"20","author":"Caplan","year":"1995","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"2","key":"2026032910223726800_ref110","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005","article-title":"General Recursion via Coinductive Types","volume":"1","author":"Capretta","year":"2005","journal-title":"Logical Methods in Computer Science"},{"key":"2026032910223726800_ref111","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-74464-1_5","volume-title":"Types for Proofs and Programs","author":"Capretta","year":"2007"},{"issue":"1","key":"2026032910223726800_ref112","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1006\/inco.1994.1013","article-title":"An Extension of System F with Subtyping","volume":"109","author":"Cardelli","year":"1994","journal-title":"Inf. Comput"},{"key":"2026032910223726800_ref113","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/2535838.2535883","volume-title":"Combining proofs and programs in a dependently typed language","author":"Casinghino","year":"2014"},{"key":"2026032910223726800_ref114","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1109\/ASE.2017.8115630","volume-title":"iCoq: Regression Proof Selection for Large-Scale Verification Projects","author":"Celik","year":"2017"},{"issue":"1","key":"2026032910223726800_ref115","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10817-008-9101-x","article-title":"Proof synthesis and reflection for linear arithmetic","volume":"41","author":"Chaieb","year":"2008","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref116","doi-asserted-by":"publisher","first-page":"1054","DOI":"10.1145\/3314221.3314585","volume-title":"Argosy: Verifying Layered Storage Systems with Recovery Refinement","author":"Chajed","year":"2019"},{"key":"2026032910223726800_ref117","first-page":"46","article-title":"GALILEO: A system for automating ontology evolution","volume-title":"ARCOE-11","author":"Chan","year":"2011"},{"key":"2026032910223726800_ref118","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/1863543.1863590","volume-title":"Program Verification Through Characteristic Formulae","author":"Chargu\u00e9raud","year":"2010"},{"key":"2026032910223726800_ref119","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-011-9225-2","article-title":"The Locally Nameless Representation","volume-title":"Journal of Automated Reasoning","author":"Chargu\u00e9raud","year":"2011"},{"key":"2026032910223726800_ref120","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1145\/3132747.3132776","volume-title":"Verifying a High-performance Crash-safe File System Using a Tree Specification","author":"Chen","year":"2017"},{"key":"2026032910223726800_ref121","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/2815400.2815402","volume-title":"Using Crash Hoare Logic for Certifying the FSCQ File System","author":"Chen","year":"2015"},{"key":"2026032910223726800_ref122","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/1411204.1411226","volume-title":"Parametric Higher-order Abstract Syntax for Mechanized Semantics","author":"Chlipala","year":"2008"},{"key":"2026032910223726800_ref123","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/1993498.1993526","volume-title":"PLDI","author":"Chlipala","year":"2011"},{"key":"2026032910223726800_ref124","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala","year":"2013"},{"key":"2026032910223726800_ref125","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/2500365.2500592","volume-title":"The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier","author":"Chlipala","year":"2013"},{"key":"2026032910223726800_ref126","unstructured":"Chlipala, A.\n          \n          2017. \u201cFormal Reasoning About Programs\u201d. url: http:\/\/adam.chlipala.net\/frap\/."},{"key":"2026032910223726800_ref127","unstructured":"Chlipala, A.\n          \n          2018. \u201cThe Surprising Security Benefits of End-to-End Formal Proofs\u201d. URL: https:\/\/www.cccblog.org\/2018\/06\/13\/the-surprising-security-benefits-of-end-to-end-formal-proofs\/."},{"key":"2026032910223726800_ref128","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4230\/LIPIcs.SNAPL.2017.3","volume-title":"The End of History: Using a Proof Assistant to Replace Language Design with Library Design","author":"Chlipala","year":"2017"},{"key":"2026032910223726800_ref129","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/1596550.1596565","volume-title":"Effective interactive proofs for higher-order imperative programs","author":"Chlipala","year":"2009"},{"issue":"9","key":"2026032910223726800_ref130","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1145\/3022670.2951932","article-title":"Elaborator Reflection: Extending Idris in Idris","volume":"51","author":"Christiansen","year":"2016","journal-title":"SIGPLAN Not"},{"key":"2026032910223726800_ref131","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"Chrz\u0105szcz","year":"2003"},{"issue":"2","key":"2026032910223726800_ref132","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371054","article-title":"An Unsolvable Problem of Elementary Number Theory","volume":"58","author":"Church","year":"1936","journal-title":"American Journal of Mathematics"},{"issue":"2","key":"2026032910223726800_ref133","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"key":"2026032910223726800_ref134","volume-title":"The calculi of lambda-conversion","author":"Church","year":"1941"},{"key":"2026032910223726800_ref135","doi-asserted-by":"publisher","first-page":"109","DOI":"10.4204\/EPTCS.113.11","volume-title":"A weak HOAS approach to the POPLMark Challenge","author":"Ciaffaglione","year":"2012"},{"key":"2026032910223726800_ref136","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-39634-2_8","volume-title":"Lightweight proof by reflection using a posteriori simulation of effectful computation","author":"Claret","year":"2013"},{"key":"2026032910223726800_ref137","unstructured":"cody\n          . 2015. \u201cWhy does Coq have Prop?\u201d Theoretical Computer Science Stack Exchange. URL: http:\/\/cstheory.stackexchange.com\/questions\/21836\/why-does-coq-have-prop."},{"key":"2026032910223726800_ref138","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-39634-2_17","volume-title":"Interactive Theorem Proving","author":"Cohen","year":"2013"},{"key":"2026032910223726800_ref139","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4230\/LIPIcs.TYPES.2015.5","volume-title":"Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom","author":"Cohen","year":"2018"},{"key":"2026032910223726800_ref140","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-03545-1_10","volume-title":"Certified Programs and Proofs","author":"Cohen","year":"2013"},{"issue":"2","key":"2026032910223726800_ref141","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1137\/0212016","article-title":"The Equivalence of Two Semantic Definitions: A Case Study in LCF","volume":"12","author":"Cohn","year":"1983","journal-title":"SIAM Journal on Computing"},{"key":"2026032910223726800_ref142","unstructured":"CompCert Development Team\n          . 2010. \u201cMerge of the newmem and newextcalls branches\u201d. URL: http:\/\/github.com\/AbsInt\/CompCert\/commit\/a74f6b45d72834b5b8417297017bd81424123d98."},{"key":"2026032910223726800_ref143","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"2026032910223726800_ref144","doi-asserted-by":"publisher","DOI":"10.1016\/C2009-0-27982-7","volume-title":"Engineering a compiler","author":"Cooper","year":"2011"},{"key":"2026032910223726800_ref145","unstructured":"Coq Development Team\n          . 2003. \u201cinterface GTK2 experimentale\u201d. url: http:\/\/github.com\/coq\/coq\/commit\/3fe1d8e4287."},{"key":"2026032910223726800_ref146","unstructured":"Coq Development Team\n          . 2017. \u201cCoqStyle\u201d. url: https:\/\/github.com\/coq\/coq\/wiki\/CoqStyle."},{"key":"2026032910223726800_ref147","unstructured":"Coq Development Team\n          . 2017-2019. \u201cCoqInTheClassroom\u201d. URL: http:\/\/github.com\/coq\/coq\/wiki\/CoqInTheClassroom."},{"key":"2026032910223726800_ref148","unstructured":"Coq Development Team\n          . 2018-2019. \u201cPreliminary compilation of critical bugs in stable releases of Coq\u201d. url: http:\/\/github.com\/coq\/coq\/blob\/master\/dev\/doc\/critical-bugs."},{"key":"2026032910223726800_ref149","unstructured":"Coq Development Team\n          . 1999-2018a. \u201cCoq Integrated Development Environment\u201d. URL: http:\/\/coq.inria.fr\/refman\/practical-tools\/coqide.html."},{"key":"2026032910223726800_ref150","unstructured":"Coq Development Team\n          . 1999-2018b. \u201cTactics\u201d. URL: http:\/\/coq.inria.fr\/refman\/proof-engine\/tactics.html."},{"key":"2026032910223726800_ref151","unstructured":"Coq Development Team\n          . 1999-2018c. \u201cThe Coq Commands\u201d. URL: http:\/\/coq.inria.fr\/refman\/practical-tools\/coq-commands.html."},{"key":"2026032910223726800_ref152","unstructured":"Coq Development Team\n          . 1989-2019. \u201cThe Coq Proof Assistant\u201d. URL: http:\/\/coq.inria.fr."},{"key":"2026032910223726800_ref153","unstructured":"Coq development team\n          . 2018. \u201cCoq OPAM Package Index\u201d. URL: https:\/\/coq.inria.fr\/opam\/www\/."},{"key":"2026032910223726800_ref154","unstructured":"CoqHoTT Development Team\n          . 2015-2019. \u201cThe CoqHoTT Project\u201d. URL: http:\/\/coqhott.gforge.inria.fr\/."},{"key":"2026032910223726800_ref155","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"Coquand","year":"1994"},{"key":"2026032910223726800_ref156","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-15983-5_13","volume-title":"EUROCAL \u201885","author":"Coquand","year":"1985"},{"issue":"2","key":"2026032910223726800_ref157","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"2026032910223726800_ref158","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"Coquand","year":"1990"},{"key":"2026032910223726800_ref159","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"A Declarative Language for the Coq Proof Assistant","author":"Corbineau","year":"2008"},{"key":"2026032910223726800_ref160","volume-title":"The Coq Proof assistant, Reference Manual, Version 5.10","author":"Cornes","year":"1995"},{"key":"2026032910223726800_ref161","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-61780-9_64","volume-title":"Automating inversion of inductive predicates in Coq","author":"Cornes","year":"1995"},{"key":"2026032910223726800_ref162","unstructured":"Crary, K. and R.Harper. 2014. \u201cThe Mechanization of Standard ML\u201d. URL: http:\/\/github.com\/SMLFamily\/The-Mechanization-of-Standard-ML."},{"key":"2026032910223726800_ref163","unstructured":"Cr\u00e9gut, P.\n          \n          1999-2018. \u201cOmega: A solver for quantifier-free problems in Presburger Arithmetic\u201d. URL: http:\/\/coq.inria.fr\/refman\/addendum\/omega.html."},{"issue":"1","key":"2026032910223726800_ref164","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.entcs.2005.11.024","article-title":"A Large-Scale Experiment in Executing Extracted Programs","volume":"151","author":"Cruz-Filipe","year":"2006","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2026032910223726800_ref165","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/10930755_14","volume-title":"Program Extraction from Large Proof Developments","author":"Cruz-Filipe","year":"2003"},{"key":"2026032910223726800_ref166","volume-title":"Theses","author":"Curien","year":"1995"},{"key":"2026032910223726800_ref167","first-page":"584","volume-title":"Functionality in Combinatory Logic","author":"Curry","year":"1934"},{"issue":"1","key":"2026032910223726800_ref168","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","article-title":"Hammer for Coq: Automation for Dependent Type Theory","volume":"61","author":"Czajka","year":"2018","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref169","unstructured":"Czajka, L., C.Kaliszyk, and B.Ekici. 2018. \u201cCoqHammer: Automation for Dependent Type Theory\u201d. URL: http:\/\/cl-informatik.uibk.ac.at\/cek\/coqhammer\/."},{"key":"2026032910223726800_ref170","doi-asserted-by":"publisher","first-page":"e9","DOI":"10.1017\/S0956796816000356","article-title":"The essence of ornaments","volume":"27","author":"Dagand","year":"2017","journal-title":"J. Funct. Program"},{"key":"2026032910223726800_ref171","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-63104-6_7","volume-title":"Integration of automated and interactive theorem proving in ILF","author":"Dahn","year":"1997"},{"key":"2026032910223726800_ref172","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/2508859.2516702","volume-title":"Formal Verification of Information Flow Security for a Simple ARM-based Separation Kernel","author":"Dam","year":"2013"},{"key":"2026032910223726800_ref173","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/2364527.2364546","volume-title":"Operational Semantics Using the Partiality Monad","author":"Danielsson","year":"2012"},{"issue":"1","key":"2026032910223726800_ref174","first-page":"165","article-title":"Finite sets","volume":"1","author":"Darmochwai","year":"1990","journal-title":"Formalized Mathematics"},{"issue":"2","key":"2026032910223726800_ref175","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10817-015-9324-6","article-title":"The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)","volume":"55","author":"Davis","year":"2015","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref176","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"The mathematical language Automath, its usage, and some of its extensions","author":"de Bruijn","year":"1970"},{"key":"2026032910223726800_ref177","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem","author":"de Bruijn","year":"1972"},{"key":"2026032910223726800_ref178","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0049-237X(08)70203-9","volume-title":"Selected Papers on Automath","author":"de Bruijn","year":"1994"},{"key":"2026032910223726800_ref179","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"The Lean Theorem Prover (System Description)","author":"de Moura","year":"2015"},{"key":"2026032910223726800_ref180","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data refinement: model-oriented proof methods and their comparison","author":"De Roever","year":"1998"},{"key":"2026032910223726800_ref181","unstructured":"DeepSpec Team\n          . 2013-2019. \u201cDeepSpec Project\u201d. uRL: https:\/\/deepspec.org."},{"key":"2026032910223726800_ref182","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"A Tactic Language for the System Coq","author":"Delahaye","year":"2000"},{"key":"2026032910223726800_ref183","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1145\/2048066.2048113","volume-title":"Product Lines of Theorems","author":"Delaware","year":"2011"},{"key":"2026032910223726800_ref184","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/2500365.2500587","volume-title":"Modular Monadic Meta-theory","author":"Delaware","year":"2013"},{"key":"2026032910223726800_ref185","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1145\/2676726.2677006","volume-title":"Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant","author":"Delaware","year":"2015"},{"key":"2026032910223726800_ref186","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/2429069.2429094","volume-title":"Meta-theory \u00e0 La Carte","author":"Delaware","year":"2013"},{"key":"2026032910223726800_ref187","first-page":"29","volume-title":"Reflection in logic, functional and object-oriented programming: A Short Comparative Study","author":"Demers","year":"1995"},{"key":"2026032910223726800_ref188","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1145\/512950.512970","volume-title":"Social Processes and Proofs of Theorems and Programs","author":"DeMillo","year":"1977"},{"key":"2026032910223726800_ref189","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/2034773.2034796","volume-title":"On the Bright Side of Type Classes: Instance Arguments in Agda","author":"Devriese","year":"2011"},{"key":"2026032910223726800_ref190","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/3236799","volume-title":"Generic Zero-cost Reuse for Dependent Types","author":"Diehl","year":"2018"},{"key":"2026032910223726800_ref191","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/2318202.2318210","volume-title":"Verification games: Making verification fun","author":"Dietl","year":"2012"},{"key":"2026032910223726800_ref192","volume-title":"Assertion level proofplanning with compiled strategies","author":"Dietrich","year":"2011"},{"key":"2026032910223726800_ref193","doi-asserted-by":"publisher","first-page":"776","DOI":"10.1007\/978-3-642-45221-5_52","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Dietrich","year":"2013"},{"issue":"8","key":"2026032910223726800_ref194","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded Commands, Nondeterminacy and Formal Derivation of Programs","volume":"18","author":"Dijkstra","year":"1975","journal-title":"Commun. ACM"},{"key":"2026032910223726800_ref195","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction - CADE-19","author":"Dixon","year":"2003"},{"key":"2026032910223726800_ref196","first-page":"166","volume-title":"A theory of termination via indirection","author":"Dockins","year":"2010"},{"issue":"1","key":"2026032910223726800_ref197","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/s10817-018-9460-x","article-title":"Regular Language Representations in the Constructive Type Theory of Coq","volume":"61","author":"Doczkal","year":"2018","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref198","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/SISY.2015.7325367","volume-title":"Theory exploration of binary trees","author":"Dramnesc","year":"2015"},{"key":"2026032910223726800_ref199","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1190216.1190229","volume-title":"Modular Type Classes","author":"Dreyer","year":"2007"},{"key":"2026032910223726800_ref200","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110278","volume-title":"A Metaprogramming Framework for Formal Verification","author":"Ebner","year":"2017"},{"key":"2026032910223726800_ref201","unstructured":"Eclipse Foundation\n          . 2001-2019. \u201cEclipse\u201d. URL: http:\/\/www.eclipse.org\/ide\/."},{"key":"2026032910223726800_ref202","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/2517349.2522720","volume-title":"From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels?","author":"Elphinstone","year":"2013"},{"key":"2026032910223726800_ref203","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005","volume-title":"Simple High-Level Code For Cryptographic Arithmetic - With Proofs, Without Compromises","author":"Erbsen","year":"2019"},{"key":"2026032910223726800_ref204","article-title":"A self-contained, brief and complete formulation of Voevodsky\u2019s Univalence Axiom","volume-title":"CoRR","author":"Escard\u00f3","year":"2018"},{"key":"2026032910223726800_ref205","first-page":"463","volume-title":"A fully verified executable LTL model checker","author":"Esparza","year":"2013"},{"issue":"2","key":"2026032910223726800_ref206","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s10009-017-0457-2","article-title":"Coqoon: An IDE for interactive proof development in Coq","volume":"20","author":"Faithfull","year":"2018","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2026032910223726800_ref207","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-22102-1_11","volume-title":"Proof-producing reflection for HOL","author":"Fallenstein","year":"2015"},{"key":"2026032910223726800_ref208","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1093\/0195148770.003.0019","volume-title":"Oxford Handbook of Philosophy of Mathematics and Logic","author":"Feferman","year":"2005"},{"key":"2026032910223726800_ref209","article-title":"The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks","volume-title":"CoRR","author":"Felty","year":"2015"},{"key":"2026032910223726800_ref210","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-58216-9_25","volume-title":"Generalization and reuse of tactic proofs","author":"Felty","year":"1994"},{"issue":"1","key":"2026032910223726800_ref211","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-010-9194-x","article-title":"Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax","volume":"48","author":"Felty","year":"2012","journal-title":"Journal of Automated Reasoning"},{"issue":"9","key":"2026032910223726800_ref212","doi-asserted-by":"publisher","first-page":"1507","DOI":"10.1017\/S0960129517000093","article-title":"Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions","volume":"28","author":"Felty","year":"2018","journal-title":"Mathematical Structures in Computer Science"},{"key":"2026032910223726800_ref213","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14052-5_17","volume-title":"Interactive Theorem Proving","author":"Felty","year":"2010"},{"key":"2026032910223726800_ref214","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1145\/1480881.1480922","volume-title":"POPL","author":"Feng","year":"2009"},{"key":"2026032910223726800_ref215","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1145\/1086365.1086399","volume-title":"Modular verification of concurrent assembly code with dynamic thread creation and termination","author":"Feng","year":"2005"},{"key":"2026032910223726800_ref216","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-24725-8_26","volume-title":"Programming Languages and Systems","author":"Filli\u00e2tre","year":"2004"},{"key":"2026032910223726800_ref217","volume-title":"Aspect-oriented Software Development","author":"Filman","year":"2004"},{"key":"2026032910223726800_ref218","first-page":"19","volume-title":"Assigning Meanings to Programs","author":"Floyd","year":"1967"},{"key":"2026032910223726800_ref219","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"Fox","year":"2010"},{"key":"2026032910223726800_ref220","doi-asserted-by":"publisher","first-page":"59","DOI":"10.4230\/OASIcs.PPES.2011.59","volume-title":"Bringing Theory to Practice: Predictability and Performance in Embedded Systems. Vol. 18. OpenAccess Series in Informatics (OASIcs)","author":"Fran\u00e7a","year":"2011"},{"key":"2026032910223726800_ref221","volume-title":"Grundgesetze der Arithmetik","author":"Frege","year":"1893"},{"key":"2026032910223726800_ref222","doi-asserted-by":"publisher","first-page":"15","DOI":"10.4204\/EPTCS.239.2","volume-title":"jsCoq: Towards Hybrid Theorem Proving Interfaces","author":"Gallego Arias","year":"2017"},{"key":"2026032910223726800_ref223","volume-title":"Generic Proof Tools and Finite Group Theory","author":"Garillot","year":"2011"},{"key":"2026032910223726800_ref224","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"TPHOL. Vol. 5674. LNCS","author":"Garillot","year":"2009"},{"key":"2026032910223726800_ref225","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-08434-3_20","volume-title":"Intelligent Computer Mathematics","author":"Gauthier","year":"2014"},{"key":"2026032910223726800_ref226","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-662-48899-7_26","volume-title":"Sharing HOL4 and HOL Light Proof Knowledge","author":"Gauthier","year":"2015"},{"key":"2026032910223726800_ref227","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jsc.2018","article-title":"Aligning concepts across proof assistant libraries","volume":"90","author":"Gauthier","year":"2019","journal-title":"Journal of Symbolic Computation"},{"key":"2026032910223726800_ref228","doi-asserted-by":"publisher","first-page":"125","DOI":"10.29007\/ntlb","volume-title":"TacticToe: Learning to Reason with HOL4 Tactics","author":"Gauthier","year":"2017"},{"key":"2026032910223726800_ref229","article-title":"Learning to Prove with Tactics","volume-title":"CoRR","author":"Gauthier","year":"2018"},{"issue":"1","key":"2026032910223726800_ref230","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s12046-009-0001-5","article-title":"Proof assistants: History, ideas and future","volume":"34","author":"Geuvers","year":"2009","journal-title":"Sadhana"},{"issue":"4","key":"2026032910223726800_ref231","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1006\/jsco.2002.0552","article-title":"A Constructive Algebraic Hierarchy in Coq","volume":"34","author":"Geuvers","year":"2002","journal-title":"Journal of Symbolic Computation"},{"key":"2026032910223726800_ref232","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45842-5_7","volume-title":"Types for Proofs and Programs. TYPES \u201800","author":"Geuvers","year":"2002"},{"key":"2026032910223726800_ref233","unstructured":"Giero, M., F.Wiedijk, M.Giero, and F.Wiedijk. 2003. \u201cMMode, a Mizar mode for the proof assistant Coq\u201d. URL: http:\/\/www.cs.kun.nl\/~freek\/mmode\/mmode.pdf."},{"key":"2026032910223726800_ref234","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-60579-7_3","volume-title":"Types for Proofs and Programs","author":"Gim\u00e9nez","year":"1995"},{"key":"2026032910223726800_ref235","unstructured":"GitHub\n          . 2014-2019. \u201cAtom\u201d. URL: http:\/\/atom.io\/."},{"key":"2026032910223726800_ref236","unstructured":"GNU Project\n          . 1985-2019. \u201cGNU Emacs\u201d. URL: http:\/\/www.gnu.org\/software\/emacs\/."},{"issue":"1","key":"2026032910223726800_ref237","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF01696781","article-title":"Die Vollst\u00e4ndigkeit der Axiome des logischen Funktionenkalk\u00fcls","volume":"37","author":"G\u00f6del","year":"1930","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"issue":"1","key":"2026032910223726800_ref238","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","article-title":"\u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"2026032910223726800_ref239","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/3133933","volume-title":"Verifying strong eventual consistency in distributed systems","author":"Gomes","year":"2017"},{"issue":"11","key":"2026032910223726800_ref240","first-page":"1382","article-title":"Formal proof\u2014the four-color theorem","volume":"55","author":"Gonthier","year":"2008","journal-title":"Notices of the American Mathematical Society"},{"key":"2026032910223726800_ref241","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"A Machine-Checked Proof of the Odd Order Theorem","author":"Gonthier","year":"2013"},{"issue":"2","key":"2026032910223726800_ref242","doi-asserted-by":"publisher","first-page":"95","DOI":"10.6092\/issn.1972-5787\/1979","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"2026032910223726800_ref243","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-642-32347-8_25","volume-title":"Interactive Theorem Proving","author":"Gonthier","year":"2012"},{"key":"2026032910223726800_ref244","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/2034773.2034798","volume-title":"How to Make Ad Hoc Proof Automation Less Ad Hoc","author":"Gonthier","year":"2011"},{"key":"2026032910223726800_ref245","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/3-540-57826-9_152","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"Gordon","year":"1994"},{"issue":"3","key":"2026032910223726800_ref246","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3064850","article-title":"Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types","volume":"39","author":"Gordon","year":"2017","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032910223726800_ref247","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, Language, and Interaction","author":"Gordon","year":"2000"},{"key":"2026032910223726800_ref248","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon","year":"1993"},{"key":"2026032910223726800_ref249","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1145\/512760.512773","volume-title":"A Metalanguage for Interactive Proof in LCF","author":"Gordon","year":"1978"},{"key":"2026032910223726800_ref250","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","article-title":"Edinburgh LCF: A Mechanised Logic of Computation","volume":"78","author":"Gordon","year":"1979","journal-title":"Lecture Notes in Computer Science"},{"key":"2026032910223726800_ref251","volume-title":"ANSI Common Lisp","author":"Graham","year":"1996"},{"key":"2026032910223726800_ref252","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Proving equalities in a commutative ring done right in Coq","author":"Gr\u00e9goire","year":"2005"},{"key":"2026032910223726800_ref253","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1145\/2676726.2676975","volume-title":"POPL","author":"Gu","year":"2015"},{"key":"2026032910223726800_ref254","first-page":"653","volume-title":"OSDI","author":"Gu","year":"2016"},{"key":"2026032910223726800_ref255","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1145\/3192366.3192381","volume-title":"PLDI","author":"Gu","year":"2018"},{"issue":"6","key":"2026032910223726800_ref256","doi-asserted-by":"publisher","first-page":"793","DOI":"10.3233\/JCS-160558","article-title":"Provably secure memory isolation for Linux on ARM","volume":"24","author":"Guanciale","year":"2016","journal-title":"Journal of Computer Security"},{"key":"2026032910223726800_ref257","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"Haftmann","year":"2013"},{"key":"2026032910223726800_ref258","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Code Generation via Higher-order Rewrite Systems","author":"Haftmann","year":"2010"},{"key":"2026032910223726800_ref259","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"Haftmann","year":"2007"},{"key":"2026032910223726800_ref260","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-02444-3_10","volume-title":"Types for Proofs and Programs","author":"Haftmann","year":"2009"},{"issue":"10","key":"2026032910223726800_ref261","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","article-title":"The Jordan curve theorem, formally and informally","volume":"114","author":"Hales","year":"2007","journal-title":"American Mathematical Monthly"},{"key":"2026032910223726800_ref262","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-1-4614-1129-1_9","volume-title":"The Kepler Conjecture: The Hales-Ferguson Proof","author":"Hales","year":"2011"},{"key":"2026032910223726800_ref263","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1017\/fmp.2017.1","article-title":"A Formal Proof of the Kepler Conjecture","volume-title":"Forum of Mathematics, Pi","author":"Hales","year":"2017"},{"issue":"4","key":"2026032910223726800_ref264","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1017\/S0956796899003378","article-title":"Proof-directed Debugging","volume":"9","author":"Harper","year":"1999","journal-title":"J. Funct. Program"},{"key":"2026032910223726800_ref265","unstructured":"Harper, R.\n          \n          2011. \u201cModules Matter Most\u201d. URL: https:\/\/existentialtype.wordpress.com\/2011\/04\/16\/modules-matter-most\/."},{"key":"2026032910223726800_ref266","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316576892","volume-title":"Practical foundations for programming languages","author":"Harper","year":"2016"},{"key":"2026032910223726800_ref267","volume-title":"Personal communication","author":"Harper","year":"2019"},{"issue":"1","key":"2026032910223726800_ref268","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A Framework for Defining Logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"2026032910223726800_ref269","first-page":"194","volume-title":"A Framework for Defining Logics","author":"Harper","year":"1987"},{"issue":"4","key":"2026032910223726800_ref270","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1017\/S0956796807006430","article-title":"Mechanizing metatheory in a logical framework","volume":"17","author":"Harper","year":"2007","journal-title":"Journal of Functional Programming"},{"key":"2026032910223726800_ref271","volume-title":"Technical Report","author":"Harrison","year":"1995"},{"key":"2026032910223726800_ref272","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics","author":"Harrison","year":"1996"},{"key":"2026032910223726800_ref273","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/B978-0-444-51624-4.50004-6","article-title":"History of Interactive Theorem Proving","volume":"9","author":"Harrison","year":"2014","journal-title":"Computational Logic"},{"key":"2026032910223726800_ref274","first-page":"257","volume-title":"Generalization at higher types","author":"Hasker","year":"1992"},{"key":"2026032910223726800_ref275","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-44755-5_18","volume-title":"Theorem Proving in Higher Order Logics","author":"Hemer","year":"2001"},{"key":"2026032910223726800_ref276","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39320-4_28","volume-title":"Intelligent Computer Mathematics","author":"Heras","year":"2013"},{"issue":"1","key":"2026032910223726800_ref277","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s11786-014-0173-1","article-title":"Recycling Proof Patterns in Coq: Case Studies","volume":"8","author":"Heras","year":"2014","journal-title":"Mathematics in Computer Science"},{"key":"2026032910223726800_ref278","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-45221-5_27","volume-title":"Proof-Pattern Recognition and Lemma Discovery in ACL2","author":"Heras","year":"2013"},{"key":"2026032910223726800_ref279","volume-title":"Intuitionism. An introduction","author":"Heyting","year":"1956"},{"issue":"10","key":"2026032910223726800_ref280","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An Axiomatic Basis for Computer Programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"issue":"1","key":"2026032910223726800_ref281","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/362452.362489","article-title":"Proof of a Program: FIND","volume":"14","author":"Hoare","year":"1971","journal-title":"Commun. ACM"},{"key":"2026032910223726800_ref282","unstructured":"HOL Development Team\n          . 2018. \u201cThe HOL System TUTORIAL\u201d. url: http:\/\/sourceforge.net\/projects\/hol\/files\/hol\/kananaskis-12\/kananaskis-12-tutorial.pdf?download."},{"key":"2026032910223726800_ref283","unstructured":"HOL Development Team\n          . 2016-2018. \u201cRunning hol\u201d. url: https:\/\/hol-theorem-prover.org\/guidebook\/#running-hol."},{"key":"2026032910223726800_ref284","unstructured":"HOL Light Development Team\n          . 1996-2019. \u201cHOL Light\u201d. url: http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light."},{"key":"2026032910223726800_ref285","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11541868_9","volume-title":"A Design Structure for Higher Order Quotients","author":"Homeier","year":"2005"},{"key":"2026032910223726800_ref286","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"2026032910223726800_ref287","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/BFb0012835","volume-title":"Computational metatheory in Nuprl","author":"Howe","year":"1988"},{"key":"2026032910223726800_ref288","volume-title":"GamePad: A Learning Environment for Theorem Proving","author":"Huang","year":"2019"},{"key":"2026032910223726800_ref289","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL","author":"Huffman","year":"2013"},{"key":"2026032910223726800_ref290","doi-asserted-by":"publisher","first-page":"999","DOI":"10.1007\/978-3-319-89884-1_35","volume-title":"Programming Languages and Systems","author":"Hupel","year":"2018"},{"key":"2026032910223726800_ref291","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Integrating Gandalf and HOL","author":"Hurd","year":"1999"},{"key":"2026032910223726800_ref292","first-page":"56","article-title":"First-order proof tactics in higher-order logic theorem provers","volume-title":"Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical Reports","author":"Hurd","year":"2003"},{"issue":"3","key":"2026032910223726800_ref293","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/503502.503505","article-title":"Featherweight Java: A minimal core calculus for Java and GJ","volume":"23","author":"Igarashi","year":"2001","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032910223726800_ref294","unstructured":"Inria\n          . 1999-2018. \u201cThe Tactic Language\u201d. url: https:\/\/coq.inria.fr\/refman\/proof-engine\/ltac.html."},{"issue":"1","key":"2026032910223726800_ref295","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","article-title":"Productive Use of Failure in Inductive Proof","volume":"16","author":"Ireland","year":"1996","journal-title":"J. Au-tom. Reasoning"},{"key":"2026032910223726800_ref296","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Irvine","year":"2016"},{"key":"2026032910223726800_ref297","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Irvine","year":"2016"},{"key":"2026032910223726800_ref298","first-page":"2235","volume-title":"Advances in Neural Information Processing Systems 29","author":"Irving","year":"2016"},{"key":"2026032910223726800_ref299","unstructured":"Isabelle Development Team\n          . 1994-2019. \u201cIsabelle\u201d. url: http:\/\/isabelle.in.tum.de."},{"key":"2026032910223726800_ref300","first-page":"8","volume-title":"Establishing Browser Security Guarantees Through Formal Shim Verification","author":"Jang","year":"2012"},{"key":"2026032910223726800_ref301","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.infsof.2014.11.005","article-title":"An empirical research agenda for understanding formal methods productivity","volume":"60","author":"Jeffery","year":"2015","journal-title":"Information and Software Technology"},{"key":"2026032910223726800_ref302","unstructured":"JetBrains\n          . 2001-2019. \u201cIntelliJ IDEA\u201d. url: http:\/\/www.jetbrains.com\/idea\/."},{"key":"2026032910223726800_ref303","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-66107-0_1","volume-title":"Automated Theory Exploration for Interactive Theorem Proving","author":"Johansson","year":"2017"},{"key":"2026032910223726800_ref304","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-08434-3_9","article-title":"Hipster: Integrating Theory Exploration in a Proof Assistant","volume-title":"CoRR","author":"Johansson","year":"2014"},{"key":"2026032910223726800_ref305","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30142-4_12","volume-title":"Theorem Reuse by Proof Term Transformation","author":"Johnsen","year":"2004"},{"key":"2026032910223726800_ref306","first-page":"321","article-title":"Specification and Design of (Parallel) Programs","volume-title":"IFIP Congress","author":"Jones","year":"1983"},{"key":"2026032910223726800_ref307","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-28869-2_20","volume-title":"Programming Languages and Systems","author":"Jourdan","year":"2012"},{"key":"2026032910223726800_ref308","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158154","volume-title":"RustBelt: Securing the Foundations of the Rust Programming Language","author":"Jung","year":"2017"},{"key":"2026032910223726800_ref309","doi-asserted-by":"publisher","first-page":"e20","DOI":"10.1017\/S0956796818000151","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung","year":"2018","journal-title":"Journal of Functional Programming"},{"key":"2026032910223726800_ref310","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/2676726.2676980","volume-title":"POPL","author":"Jung","year":"2015"},{"key":"2026032910223726800_ref311","first-page":"4","volume-title":"PPIG","author":"Kadoda","year":"1999"},{"key":"2026032910223726800_ref312","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3236773","volume-title":"Mtac2: Typed Tactics for Backward Reasoning in Coq","author":"Kaiser","year":"2018"},{"issue":"3","key":"2026032910223726800_ref313","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s10009-002-0081-6","article-title":"Proof engineering in the large: formal verification of Pentium 4 floating-point divider","volume":"4","author":"Kaivola","year":"2003","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"2026032910223726800_ref314","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.entcs.2006.09.021","article-title":"Web interfaces for proof assistants","volume":"174","author":"Kaliszyk","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2026032910223726800_ref315","unstructured":"Kaliszyk, C., F.Chollet, and C.Szegedy. 2017a. \u201cHolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving\u201d. In: ICLR. url: https:\/\/openreview.net\/forum?id=ryuxYmvel."},{"issue":"1","key":"2026032910223726800_ref316","doi-asserted-by":"publisher","first-page":"27","DOI":"10.6092\/issn.1972-5787\/1411","article-title":"Computing with Classical Real Numbers","volume":"2","author":"Kaliszyk","year":"2009","journal-title":"Journal of Formalized Reasoning"},{"issue":"2","key":"2026032910223726800_ref317","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","article-title":"Learning-Assisted Automated Reasoning with Flyspeck","volume":"53","author":"Kaliszyk","year":"2014","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"2026032910223726800_ref318","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","article-title":"HOL(y)Hammer: Online ATP Service for HOL Light","volume":"9","author":"Kaliszyk","year":"2015","journal-title":"Mathematics in Computer Science"},{"key":"2026032910223726800_ref319","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-319-66107-0_2","volume-title":"Interactive Theorem Proving","author":"Kaliszyk","year":"2017"},{"key":"2026032910223726800_ref320","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Kamm\u00fcller","year":"1999"},{"key":"2026032910223726800_ref321","first-page":"163","volume-title":"Closing the Gap - The Formally Verified Optimizing Compiler CompCert","author":"K\u00e4stner","year":"2017"},{"key":"2026032910223726800_ref322","unstructured":"K\u00e4stner, D., U.W\u00fcnsche, J.Barrho, M.Schlickling, B.Schommer, M.Schmidt, C.Ferdinand, X.Leroy, and S.Blazy. 2018. \u201cCompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler\u201d. In: ERTS 2018: Embedded Real Time Software and Systems. SEE. url: https:\/\/hal.inria.fr\/hal-01643290."},{"key":"2026032910223726800_ref323","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1145\/2983990.2983996","volume-title":"OOPSLA","author":"Kell","year":"2016"},{"key":"2026032910223726800_ref324","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-71237-6_14","volume-title":"APLAS","author":"Kim","year":"2017"},{"key":"2026032910223726800_ref325","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-06410-9_2","volume-title":"Proof Engineering Considered Essential","author":"Klein","year":"2014"},{"key":"2026032910223726800_ref326","unstructured":"Klein, G.\n          \n          2015. \u201cGerwin\u2019s Style Guide for Isabelle\/HOL\u201d. url: https:\/\/proofcraft.org\/blog\/isabelle-style.html."},{"issue":"1","key":"2026032910223726800_ref327","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2560537","article-title":"Comprehensive Formal Verification of an OS Microkernel","volume":"32","author":"Klein","year":"2014","journal-title":"ACM Trans. Comput. Syst"},{"issue":"10","key":"2026032910223726800_ref328","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/3230627","article-title":"Formally Verified Software in the Real World","volume":"61","author":"Klein","year":"2018","journal-title":"Commun. ACM"},{"issue":"2104","key":"2026032910223726800_ref329","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0404","article-title":"Provably trustworthy systems","volume":"375","author":"Klein","year":"2017","journal-title":"Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences"},{"key":"2026032910223726800_ref330","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"seL4: Formal Verification of an OS Kernel","author":"Klein","year":"2009"},{"key":"2026032910223726800_ref331","unstructured":"Klein, G., T.Nipkow, L.Paulson, and R.Thiemann. 2004-2019. \u201cArchive of Formal Proofs: Submission Guidelines\u201d. url: https:\/\/www.isa-afp.org\/submitting.html."},{"key":"2026032910223726800_ref332","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1017\/S0956796816000307","article-title":"Programming with ornaments","volume-title":"Journal of Functional Programming","author":"Ko","year":"2016"},{"key":"2026032910223726800_ref333","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-94-017-0435-9_8","volume-title":"Automated Deduction \u2014 A Basis for Applications","author":"Kolbe","year":"1998"},{"key":"2026032910223726800_ref334","doi-asserted-by":"publisher","first-page":"15","DOI":"10.4204\/EPTCS.118.2","volume-title":"Machine Learning in Proof General: Interfacing Interfaces","author":"Komendantskaya","year":"2012"},{"key":"2026032910223726800_ref335","volume-title":"AVID: A system for the interactive development of verifiably correct programs","author":"Krafft","year":"1981"},{"key":"2026032910223726800_ref336","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3236772","volume-title":"MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic","author":"Krebbers","year":"2018"},{"key":"2026032910223726800_ref337","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/3009837.3009855","volume-title":"POPL","author":"Krebbers","year":"2017"},{"key":"2026032910223726800_ref338","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kroening","year":"2008","edition":"1st"},{"key":"2026032910223726800_ref339","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"K\u00fchlwein","year":"2013"},{"key":"2026032910223726800_ref340","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31365-3_30","volume-title":"Automated Reasoning","author":"K\u00fchlwein","year":"2012"},{"key":"2026032910223726800_ref341","volume-title":"Self-compilation and self-verification","author":"Kumar","year":"2015"},{"key":"2026032910223726800_ref342","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/2535838.2535841","volume-title":"CakeML: A Verified Implementation of ML","author":"Kumar","year":"2014"},{"key":"2026032910223726800_ref343","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/HOL.1991.596284","volume-title":"Integrating a first-order automatic prover in the HOL environment","author":"Kumar","year":"1991"},{"key":"2026032910223726800_ref344","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9454-8","article-title":"A Consistent Foundation for Isabelle\/HOL","volume-title":"Journal of Automated Reasoning","author":"Kuncar","year":"2018"},{"key":"2026032910223726800_ref345","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","author":"Lammich","year":"2013"},{"key":"2026032910223726800_ref346","first-page":"253","volume-title":"Refinement to imperative\/HOL","author":"Lammich","year":"2015"},{"key":"2026032910223726800_ref347","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158133","volume-title":"Generating good generators for inductive relations","author":"Lampropoulos","year":"2017"},{"key":"2026032910223726800_ref348","unstructured":"Lean Development Team\n          . 2014-2017. \u201cTheorem Proving in Lean\u201d. URL: http:\/\/leanprover.github.io\/tutorial\/."},{"key":"2026032910223726800_ref349","unstructured":"Lean Development Team\n          . 2017-2018. \u201cJavascript interface to the Lean server\u201d. URL: http:\/\/github.com\/leanprover\/lean-client-js."},{"key":"2026032910223726800_ref350","unstructured":"Lean Development Team\n          . 2016-2019. \u201cLean for VS Code\u201d. URL: http:\/\/github.com\/leanprover\/vscode-lean."},{"key":"2026032910223726800_ref351","volume-title":"The Art of Discovery","author":"Leibniz","year":"1685"},{"key":"2026032910223726800_ref352","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino","year":"2010"},{"key":"2026032910223726800_ref353","doi-asserted-by":"publisher","first-page":"3063","DOI":"10.1145\/2702123.2702302","volume-title":"Polymorphic blocks: Formalism-inspired UI for structured connectors","author":"Lerner","year":"2015"},{"key":"2026032910223726800_ref354","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"POPL","author":"Leroy","year":"2006"},{"key":"2026032910223726800_ref355","volume-title":"Research report","author":"Leroy","year":"2007"},{"issue":"7","key":"2026032910223726800_ref356","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","article-title":"Formal Verification of a Realistic Compiler","volume":"52","author":"Leroy","year":"2009","journal-title":"Commun. ACM"},{"key":"2026032910223726800_ref357","unstructured":"Leroy, X.\n          \n          2015. \u201cUsing Coq\u2019s evaluation mechanisms in anger\u201d. uRL: http:\/\/gallium.inria.fr\/blog\/coq-eval\/."},{"key":"2026032910223726800_ref358","unstructured":"Leroy, X., A. W.Appel, S.Blazy, and G.Stewart. 2012. \u201cThe CompCert Memory Model, Version 2\u201d. Research ReportNo. RR-7987. INRIA. 26. URL: https:\/\/hal.inria.fr\/hal-00703441."},{"key":"2026032910223726800_ref359","unstructured":"Leroy, X.\n          \n          2017. \u201cThe formal verification of compilers\u201d. URL: https:\/\/deepspec.org\/event\/dsss17\/leroy-dsss17.pdf."},{"key":"2026032910223726800_ref360","first-page":"287","volume-title":"Improving Coq propositional reasoning using a lazy CNF conversion scheme","author":"Lescuyer","year":"2009"},{"key":"2026032910223726800_ref361","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"Letouzey","year":"2003"},{"key":"2026032910223726800_ref362","volume-title":"Programmation fonctionnelle certifiee - L\u2019extraction de programmes dans l\u2019assistant Coq","author":"Letouzey","year":"2004"},{"key":"2026032910223726800_ref363","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Coq Extraction, an Overview","author":"Letouzey","year":"2008"},{"key":"2026032910223726800_ref364","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1145\/2429069.2429134","volume-title":"POPL","author":"Ley-Wild","year":"2013"},{"key":"2026032910223726800_ref365","article-title":"Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC","volume-title":"CoRR","author":"Lin","year":"2016"},{"key":"2026032910223726800_ref366","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/11617990_10","volume-title":"A Tool for Automated Theorem Proving in Agda","author":"Lindblad","year":"2006"},{"key":"2026032910223726800_ref367","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-19829-8_17","volume-title":"Formal Methods: Foundations and Applications","author":"Liu","year":"2011"},{"key":"2026032910223726800_ref368","doi-asserted-by":"publisher","first-page":"85","DOI":"10.29007\/8mwc","volume-title":"Deep Network Guided Proof Search","author":"Loos","year":"2017"},{"issue":"1","key":"2026032910223726800_ref369","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","article-title":"Coercive subtyping","volume":"9","author":"Luo","year":"1999","journal-title":"Journal of Logic and Computation"},{"key":"2026032910223726800_ref370","volume-title":"Tech. rep","author":"Lynch","year":"1994"},{"key":"2026032910223726800_ref371","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1145\/512644.512670","volume-title":"Using Dependent Types to Express Modular Structure","author":"MacQueen","year":"1986"},{"key":"2026032910223726800_ref372","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-45842-5_12","volume-title":"Changing Data Structures in Type Theory: A Study of Natural Numbers","author":"Magaud","year":"2002"},{"key":"2026032910223726800_ref373","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-39634-2_5","volume-title":"Interactive Theorem Proving. Vol. 7998. LNCS","author":"Mahboubi","year":"2013"},{"key":"2026032910223726800_ref374","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-662-49498-1_21","volume-title":"Extensible and Efficient Automation Through Reflective Tactics","author":"Malecha","year":"2016"},{"key":"2026032910223726800_ref375","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/1706299.1706329","volume-title":"Toward a Verified Relational Database Management System","author":"Malecha","year":"2010"},{"key":"2026032910223726800_ref376","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Logic, Methodology and Philosophy of Science VI. Vol. 104. Studies in Logic and the Foundations of Mathematics","author":"Martin-L\u00f6f","year":"1982"},{"key":"2026032910223726800_ref377","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"2026032910223726800_ref378","doi-asserted-by":"publisher","first-page":"722","DOI":"10.1109\/ICSE.2015.85","volume-title":"Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification","author":"Matichuk","year":"2015"},{"key":"2026032910223726800_ref379","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","article-title":"Eisbach: A Proof Method Language for Isabelle","volume":"56","author":"Matichuk","year":"2015","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref380","article-title":"The Eisbach user manual","volume-title":"Isabelle Community","author":"Matichuk","year":"2015"},{"key":"2026032910223726800_ref381","first-page":"236","volume-title":"Inverting inductively defined relations in LEGO","author":"McBride","year":"1996"},{"key":"2026032910223726800_ref382","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"McBride","year":"2002"},{"key":"2026032910223726800_ref383","unstructured":"McBride, C.\n          \n          2011. \u201cOrnamental algebras, algebraic ornaments\u201d. url: http:\/\/plv.mpi-sws.org\/plerg\/papers\/mcbride-ornaments-2up.pdf."},{"key":"2026032910223726800_ref384","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-319-19797-5_13","volume-title":"Mathematics of Program Construction","author":"McBride","year":"2015"},{"issue":"4","key":"2026032910223726800_ref385","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","article-title":"Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I","volume":"3","author":"McCarthy","year":"1960","journal-title":"Commun. ACM"},{"key":"2026032910223726800_ref386","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0049-237X(08)72018-4","volume-title":"Computer Programming and Formal Systems","author":"McCarthy","year":"1963"},{"key":"2026032910223726800_ref387","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"Practical tactics for separation logic","author":"McCreight","year":"2009"},{"key":"2026032910223726800_ref388","first-page":"2","volume-title":"Tool Demonstration: An IDE for Programming and Proving in Idris","author":"Mehnert","year":"2014"},{"key":"2026032910223726800_ref389","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"CADE. Vol. 2741. LNCS","author":"Mehta","year":"2003"},{"key":"2026032910223726800_ref390","unstructured":"Microsoft\n          . 1997-2019. \u201cVisual Studio\u201d. URL: http:\/\/visualstudio.microsoft.com\/."},{"key":"2026032910223726800_ref391","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9483-3","article-title":"Mechanized Metatheory Revisited","volume-title":"Journal of Auto-mated Reasoning","author":"Miller","year":"2018"},{"key":"2026032910223726800_ref392","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/800235.807067","volume-title":"Implementation and Applications of Scott\u2019s Logic for Computable Functions","author":"Milner","year":"1972"},{"key":"2026032910223726800_ref393","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"Milner","year":"1997"},{"key":"2026032910223726800_ref394","first-page":"51","article-title":"Proving compiler correctness in a mechanized logic","volume":"7","author":"Milner","year":"1972","journal-title":"Machine Intelligence"},{"issue":"1","key":"2026032910223726800_ref395","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3105906","article-title":"Automatic Software Repair: A Bibliography","volume":"51","author":"Monperrus","year":"2018","journal-title":"ACM Comput. Surv"},{"key":"2026032910223726800_ref396","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1145\/2254064.2254111","volume-title":"RockSalt: Better, Faster, Stronger SFI for the x86","author":"Morrisett","year":"2012"},{"key":"2026032910223726800_ref397","volume-title":"Proof Weaving","author":"Mulhern","year":"2006"},{"key":"2026032910223726800_ref398","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/3167089","volume-title":"CPP","author":"Mullen","year":"2018"},{"key":"2026032910223726800_ref399","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-62075-6_7","volume-title":"Intelligent Computer Mathematics","author":"M\u00fcller","year":"2017"},{"key":"2026032910223726800_ref400","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/2628136.2628143","volume-title":"Lem: Reusable Engineering of Real-world Semantics","author":"Mulligan","year":"2014"},{"key":"2026032910223726800_ref401","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/2593882.2593898","volume-title":"How Programming Languages Will Co-evolve with Software Engineering: A Bright Decade Ahead","author":"Murphy-Hill","year":"2014"},{"key":"2026032910223726800_ref402","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/SecDev.2018.00009","article-title":"BP: Formal Proofs, the Fine Print and Side Effects","volume-title":"IEEE Cybersecurity Development (SecDev)","author":"Murray","year":"2018"},{"key":"2026032910223726800_ref403","unstructured":"Myreen, M. O.\n          \n          2008-2018. \u201cGuide to HOL4 interaction and basic proofs\u201d. URL: http:\/\/hol-theorem-prover.org\/HOL-interaction.pdf."},{"key":"2026032910223726800_ref404","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/2364527.2364545","volume-title":"Proof-producing Synthesis of ML from Higher-order Logic","author":"Myreen","year":"2012"},{"key":"2026032910223726800_ref405","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/3238147.3238210","volume-title":"PaMpeR: Proof Method Recommendation System for Isabelle\/HOL","author":"Nagashima","year":"2018"},{"key":"2026032910223726800_ref406","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/978-3-319-63046-5_32","volume-title":"Automated Deduction - CADE 26","author":"Nagashima","year":"2017"},{"key":"2026032910223726800_ref407","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"Nanevski","year":"2014"},{"key":"2026032910223726800_ref408","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/1411204.1411237","volume-title":"Ynot: Dependent Types for Imperative Programs","author":"Nanevski","year":"2008"},{"issue":"3","key":"2026032910223726800_ref409","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/1352582.1352591","article-title":"Contextual modal type theory","volume":"9","author":"Nanevski","year":"2008","journal-title":"ACM Transactions on Computational Logic"},{"key":"2026032910223726800_ref410","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1145\/1706299.1706331","volume-title":"Structuring the Verification of Heap-manipulating Programs","author":"Nanevski","year":"2010"},{"key":"2026032910223726800_ref411","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30142-4_17","volume-title":"A decision procedure for geometry in Coq","author":"Narboux","year":"2004"},{"key":"2026032910223726800_ref412","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/2784731.2784764","volume-title":"Pilsner: A Compositionally Verified Compiler for a Higher-order Imperative Language","author":"Neis","year":"2015"},{"key":"2026032910223726800_ref413","volume-title":"Tech. rep","author":"Newey","year":"1973"},{"issue":"1","key":"2026032910223726800_ref414","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/BF01887212","article-title":"Term rewriting and beyond-theorem proving in Isabelle","volume":"1","author":"Nipkow","year":"1989","journal-title":"Formal Aspects of Computing"},{"key":"2026032910223726800_ref415","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1109\/LICS.1990.113754","volume-title":"Proof transformations for equational theories","author":"Nipkow","year":"1990"},{"key":"2026032910223726800_ref416","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"Nipkow","year":"2014"},{"key":"2026032910223726800_ref417","unstructured":"nLab authors\n          . 2019a. \u201cequality\u201d. url: http:\/\/ncatlab.org\/nlab\/show\/equality."},{"key":"2026032910223726800_ref418","unstructured":"nLab authors\n          . 2019b. \u201cfoundation of mathematics\u201d. url: http:\/\/ncatlab.org\/nlab\/show\/foundation%20of%20mathematics."},{"key":"2026032910223726800_ref419","unstructured":"nLab authors\n          . 2019c. \u201cintensional type theory\u201d. url: http:\/\/ncatlab.org\/nlab\/show\/intensional%20type%20theory."},{"key":"2026032910223726800_ref420","unstructured":"Norell, U.\n          \n          2016. \u201cAgda reflection overhaul\u201d. url: http:\/\/lists.chalmers.se\/pipermail\/agda\/2016\/008414.html."},{"key":"2026032910223726800_ref421","unstructured":"Norell, U.\n          \n          2015-2019. \u201cagda-prelude\u201d. url: http:\/\/github.com\/UlfNorell\/agda-prelude."},{"key":"2026032910223726800_ref422","article-title":"COGENT: Certified Compilation for a Functional Systems Language","volume-title":"CoRR","author":"O\u2019Connor","year":"2016"},{"key":"2026032910223726800_ref423","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11541868_16","volume-title":"Essential Incompleteness of Arithmetic Verified by Coq","author":"O\u2018Connor","year":"2005"},{"issue":"1","key":"2026032910223726800_ref424","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","article-title":"Resources, concurrency, and local reasoning","volume":"375","author":"O\u2018Hearn","year":"2007","journal-title":"Theor. Comput. Sci"},{"key":"2026032910223726800_ref425","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"CSL. Vol. 2142. LNCS","author":"O\u2018Hearn","year":"2001"},{"key":"2026032910223726800_ref426","volume-title":"Refactoring: A program restructuring aid in designing object-oriented application frameworks","author":"Opdyke","year":"1992"},{"key":"2026032910223726800_ref427","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11541868_18","volume-title":"Theorem Proving in Higher Order Logics","author":"Oury","year":"2005"},{"key":"2026032910223726800_ref428","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78739-6_1","article-title":"A sound semantics for OCaml Light","volume-title":"Programming Languages and Systems","author":"Owens","year":"2008"},{"key":"2026032910223726800_ref429","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1145\/3213846.3213877","volume-title":"ISSTA","author":"Palmskog","year":"2018"},{"key":"2026032910223726800_ref430","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-22102-1_22","volume-title":"Foundational Property-Based Testing","author":"Paraskevopoulou","year":"2015"},{"key":"2026032910223726800_ref431","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/75277.75285","volume-title":"Extracting F-omega\u2019s Programs from Proofs in the Calculus of Constructions","author":"Paulin-Mohring","year":"1989"},{"key":"2026032910223726800_ref432","first-page":"7","volume-title":"Extraction de programmes dans le Calcul des Constructions","author":"Paulin-Mohring","year":"1989"},{"key":"2026032910223726800_ref433","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"Paulin-Mohring","year":"1993"},{"issue":"5","key":"2026032910223726800_ref434","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","article-title":"Synthesis of ML programs in the system Coq","volume":"15","author":"Paulin-Mohring","year":"1993","journal-title":"Journal of Symbolic Computation"},{"key":"2026032910223726800_ref435","volume-title":"Tech. rep","author":"Paulson","year":"1983"},{"key":"2026032910223726800_ref436","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-13346-1_10","volume-title":"Semantics of Data Types","author":"Paulson","year":"1984"},{"key":"2026032910223726800_ref437","volume-title":"Tech. rep","author":"Paulson","year":"1988"},{"key":"2026032910223726800_ref438","article-title":"Isabelle: The Next 700 Theorem Provers","volume-title":"CoRR","author":"Paulson","year":"1993"},{"key":"2026032910223726800_ref439","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","article-title":"Isabelle: A Generic Theorem Prover","volume":"828","author":"Paulson","year":"1994","journal-title":"Lecture Notes in Computer Science"},{"issue":"2","key":"2026032910223726800_ref440","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1093\/logcom\/7.2.175","article-title":"Mechanizing Coinduction and Corecursion in Higher-order Logic","volume":"7","author":"Paulson","year":"1997","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"2026032910223726800_ref441","doi-asserted-by":"publisher","first-page":"73","DOI":"10.3217\/jucs-005-03-0073","article-title":"A generic tableau prover and its integration with Isabelle","volume":"5","author":"Paulson","year":"1999","journal-title":"Journal of Universal Computer Science"},{"issue":"4","key":"2026032910223726800_ref442","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/1183278.1183280","article-title":"Defining Functions on Equivalence Classes","volume":"7","author":"Paulson","year":"2006","journal-title":"ACM Trans. Comput. Logic"},{"key":"2026032910223726800_ref443","first-page":"1","volume-title":"Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers","author":"Paulson","year":"2012"},{"key":"2026032910223726800_ref444","article-title":"Ltac2: Tactical Warfare","volume-title":"CoqPL 2019","author":"P\u00e9drot","year":"2019"},{"key":"2026032910223726800_ref445","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-70096-0_1","volume-title":"Neural Information Processing","author":"Peng","year":"2017"},{"key":"2026032910223726800_ref446","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/53990.54010","volume-title":"Higher-order Abstract Syntax","author":"Pfenning","year":"1988"},{"key":"2026032910223726800_ref447","unstructured":"Pfenning, F.\n          \n          2010. \u201cLecture Notes on Proofs as Programs: Lecture 2\u201d. URL: http:\/\/www.cs.cmu.edu\/~fp\/courses\/15816-s10\/lectures\/02-pap.pdf."},{"key":"2026032910223726800_ref448","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BFb0040259","volume-title":"Mathematical Foundations of Programming Semantics","author":"Pfenning","year":"1990"},{"key":"2026032910223726800_ref449","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"System Description: Twelf \u2014 A Meta-Logical Framework for Deductive Systems","author":"Pfenning","year":"1999"},{"key":"2026032910223726800_ref450","unstructured":"PG development team\n          . 2016. \u201cProof General 4.4.1 pre Documentation\u201d. URL: https:\/\/proofgeneral.github.io\/doc\/userman\/."},{"key":"2026032910223726800_ref451","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/1389449.1389469","volume-title":"Programming with proofs and explicit contexts","author":"Pientka","year":"2008"},{"key":"2026032910223726800_ref452","volume-title":"Types and programming languages","author":"Pierce","year":"2002"},{"key":"2026032910223726800_ref453","volume-title":"Personal communication","author":"Pierce","year":"2017"},{"key":"2026032910223726800_ref454","volume-title":"Personal communication","author":"Pierce","year":"2019"},{"key":"2026032910223726800_ref455","volume-title":"Software Foundations","author":"Pierce","year":"2014"},{"key":"2026032910223726800_ref456","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.44331","volume-title":"Company-Coq: Taking Proof General one step closer to a real IDE","author":"Pit-Claudel","year":"2016"},{"key":"2026032910223726800_ref457","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290382","article-title":"Bridging the gap between programming languages and hardware weak memory models","volume":"69","author":"Podkopaev","year":"2019","journal-title":"PACMPL"},{"key":"2026032910223726800_ref458","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/3-540-60579-7_8","volume-title":"Types for Proofs and Programs","author":"Pollack","year":"1995"},{"key":"2026032910223726800_ref459","volume-title":"Twenty Five Years of Constructive Type Theory","author":"Pollack","year":"1998"},{"key":"2026032910223726800_ref460","volume-title":"Conception et r\u00c9alisation d\u2019outils d\u2019aide au d\u00c9veloppement de grosses th\u00c9ories dans les syst\u00e8mes de preuves interactifs","author":"Pons","year":"1999"},{"key":"2026032910223726800_ref461","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/j.entcs.2008.12.120","article-title":"System description: Delphin-a functional programming language for deductive systems","volume":"228","author":"Poswolsky","year":"2009","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2026032910223726800_ref462","unstructured":"Pouillard, N.\n          \n          2012. \u201cagda-tactics: Semiring\u201d. url: http:\/\/github.com\/xplat\/agda-tactics\/blob\/master\/Tactics\/Nat\/Semiring.agda."},{"key":"2026032910223726800_ref463","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/125826.125848","volume-title":"The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis","author":"Pugh","year":"1991"},{"key":"2026032910223726800_ref464","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/2771783.2771791","volume-title":"An Analysis of Patch Plausibility and Correctness for Generate-and-validate Patch Generation Systems","author":"Qi","year":"2015"},{"key":"2026032910223726800_ref465","doi-asserted-by":"publisher","first-page":"119","DOI":"10.4204\/EPTCS.266.8","volume-title":"QWIRE Practice: Formal Verification of Quantum Circuits in Coq","author":"Rand","year":"2017"},{"key":"2026032910223726800_ref466","unstructured":"RedPRL Development Team\n          . 2015-2018. \u201cThe RedPRL Proof Assistant\u201d. url: http:\/\/www.redprl.org."},{"key":"2026032910223726800_ref467","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"LICS","author":"Reynolds","year":"2002"},{"key":"2026032910223726800_ref468","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1145\/2594291.2594338","volume-title":"Automating Formal Proofs for Reactive Systems","author":"Ricketts","year":"2014"},{"key":"2026032910223726800_ref469","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/2815400.2815411","volume-title":"SibylFS: Formal Specification and Oracle-based Testing for POSIX and Real-world File Systems","author":"Ridge","year":"2015"},{"key":"2026032910223726800_ref470","unstructured":"Ringer, T. and N.Yazdani. 2018. \u201cPUMPKIN-git\u201d. url: http:\/\/github.com\/uwplse\/PUMPKIN-git."},{"key":"2026032910223726800_ref471","doi-asserted-by":"publisher","DOI":"10.1145\/3167094","volume-title":"Adapting Proof Automation to Adapt Proofs","author":"Ringer","year":"2018"},{"key":"2026032910223726800_ref472","article-title":"Ornaments for Proof Reuse in Coq","volume-title":"Interactive Theorem Proving","author":"Ringer","year":"2019"},{"key":"2026032910223726800_ref473","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_20","volume-title":"A Framework for the Automatic Formal Verification of Refinement from Cogent to C","author":"Rizkallah","year":"2016"},{"key":"2026032910223726800_ref474","volume-title":"Front-end tooling for building and maintaining dependently-typed functional programs","author":"Robert","year":"2018"},{"key":"2026032910223726800_ref475","unstructured":"Robert, V. and S.Lerner. 2014-2016. \u201cPeaCoq\u201d. url: http:\/\/goto.ucsd.edu\/peacoq\/."},{"issue":"1","key":"2026032910223726800_ref476","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A Machine-Oriented Logic Based on the Resolution Principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"2026032910223726800_ref477","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-43144-4_32","volume-title":"CoqPIE: An IDE Aimed at Improving Proof Development Productivity","author":"Roe","year":"2016"},{"key":"2026032910223726800_ref478","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1145\/2983990.2984008","volume-title":"Type Soundness for Dependent Object Types","author":"Rompf","year":"2016"},{"key":"2026032910223726800_ref479","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/800216.806586","volume-title":"Design and Verification of Secure Systems","author":"Rushby","year":"1981"},{"key":"2026032910223726800_ref480","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1112\/plms\/s2-4.1.29","volume-title":"On Some Difficulties in the Theory of Transfinite Numbers and Order Types","author":"Russell","year":"1906"},{"key":"2026032910223726800_ref481","volume-title":"Introduction to Mathematical Philosophy","author":"Russell","year":"1918"},{"key":"2026032910223726800_ref482","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/263699.263742","volume-title":"Typing Algorithm in Type Theory with Inheritance","author":"Saibi","year":"1997"},{"key":"2026032910223726800_ref483","volume-title":"Outils G\u00e9n\u00e9riques de Mod\u00e9lisation et de D\u00e9monstration pour la Formalisation des Math\u00e9matiques en Th\u00e9orie des Types: application \u00e0 la Th\u00e9orie des Cat\u00e9gories","author":"Saibi","year":"1999"},{"key":"2026032910223726800_ref484","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi","year":"2011"},{"key":"2026032910223726800_ref485","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-319-22102-1_24","volume-title":"Autosubst: Reasoning with de Bruijn terms and parallel substitutions","author":"Sch\u00e4fer","year":"2015"},{"key":"2026032910223726800_ref486","first-page":"152","volume-title":"A verified prover based on ordered resolution","author":"Schlichtkrull","year":"2019"},{"key":"2026032910223726800_ref487","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BFb0060636","volume-title":"Constructive validity","author":"Scott","year":"1970"},{"issue":"1","key":"2026032910223726800_ref488","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","article-title":"A type-theoretical alternative to ISWIM, CUCH, OWHY","volume":"121","author":"Scott","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"2026032910223726800_ref489","article-title":"Congruence Closure in Intensional Type Theory","volume-title":"CoRR","author":"Selsam","year":"2017"},{"key":"2026032910223726800_ref490","first-page":"3047","volume-title":"Developing Bug-free Machine Learning Systems with Formal Mathematics","author":"Selsam","year":"2017"},{"key":"2026032910223726800_ref491","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/2737924.2737964","volume-title":"Mechanized Verification of Fine-grained Concurrent Programs","author":"Sergey","year":"2015"},{"key":"2026032910223726800_ref492","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158116","volume-title":"Programming and Proving with Distributed Protocols","author":"Sergey","year":"2017"},{"issue":"1","key":"2026032910223726800_ref493","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","article-title":"Ott: Effective tool support for the working semanticist","volume":"20","author":"Sewell","year":"2010","journal-title":"Journal of Functional Programming"},{"issue":"5","key":"2026032910223726800_ref494","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1007\/s11241-017-9286-3","article-title":"High-assurance timing analysis for a high-assurance real-time operating system","volume":"53","author":"Sewell","year":"2017","journal-title":"Real-Time Systems"},{"issue":"4","key":"2026032910223726800_ref495","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10817-006-9027-0","article-title":"\u201cRippling: Meta-Level Guidance for Mathematical Reasoning, \u201c by Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland, Cambridge University Press, 2005","volume":"35","author":"Shah","year":"2005","journal-title":"J. Autom. Reasoning"},{"key":"2026032910223726800_ref496","unstructured":"Shaw, M., J.Aldrich, T. D.Breaux, D.Garlan, C.K\u00e4stner, C.Le Goues, and W. L.Scherlis. 2015. \u201cSeminal Papers in Software Engineering: The Carnegie Mellon Canonical Collection\u201d. url: http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/isr2015\/CMU-ISR-15-107.pdf."},{"key":"2026032910223726800_ref497","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/3-540-57826-9_154","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"Slind","year":"1994"},{"key":"2026032910223726800_ref498","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/BFb0028401","volume-title":"Theorem Proving in Higher Order Logics","author":"Slotosch","year":"1997"},{"key":"2026032910223726800_ref499","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Smith","year":"2018"},{"key":"2026032910223726800_ref500","volume-title":"Lectures on the Curry-Howard isomorphism","author":"S\u00f8rensen","year":"2006"},{"key":"2026032910223726800_ref501","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-14052-5_29","volume-title":"Interactive Theorem Proving","author":"Sozeau","year":"2010"},{"key":"2026032910223726800_ref502","volume-title":"Tech. rep","author":"Sozeau","year":"2019"},{"key":"2026032910223726800_ref503","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"First-Class Type Classes","author":"Sozeau","year":"2008"},{"key":"2026032910223726800_ref504","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-319-08970-6_32","volume-title":"Interactive Theorem Proving","author":"Sozeau","year":"2014"},{"issue":"4","key":"2026032910223726800_ref505","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","article-title":"Type classes for mathematics in type theory","volume":"21","author":"Spitters","year":"2011","journal-title":"Mathematical Structures in Computer Science"},{"key":"2026032910223726800_ref506","volume-title":"Proof Search in Type Theory","author":"Spiwack","year":"2010"},{"key":"2026032910223726800_ref507","unstructured":"Spiwack, A.\n          \n          2016. \u201cInside the design of a tactic system\u201d. url: https:\/\/github.com\/aspiwack\/tacengine\/releases\/download\/v0.1-draft\/tacengine.pdf."},{"key":"2026032910223726800_ref508","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/1863543.1863591","volume-title":"VeriML: Typed Computation of Logical Terms Inside a Language with Effects","author":"Stampoulis","year":"2010"},{"key":"2026032910223726800_ref509","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2652524.2652551","volume-title":"Productivity for Proof Engineering","author":"Staples","year":"2014"},{"key":"2026032910223726800_ref510","doi-asserted-by":"publisher","first-page":"1257","DOI":"10.1109\/ICSE.2013.6606692","volume-title":"Formal Specifications Better Than Function Points for Code Sizing","author":"Staples","year":"2013"},{"key":"2026032910223726800_ref511","article-title":"Algebraic Foundations of Proof Refinement","volume-title":"CoRR","author":"Sterling","year":"2017"},{"key":"2026032910223726800_ref512","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1145\/2676726.2676985","volume-title":"POPL","author":"Stewart","year":"2015"},{"issue":"1","key":"2026032910223726800_ref513","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1023\/A:1010000313106","article-title":"Fundamental Concepts in Programming Languages","volume":"13","author":"Strachey","year":"2000","journal-title":"Higher-Order and Symbolic Computation"},{"key":"2026032910223726800_ref514","unstructured":"StructTact Development Team\n          . 2016-2019. \u201cStructTact\u201d. url: http:\/\/github.com\/uwplse\/StructTact."},{"key":"2026032910223726800_ref515","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1017\/S0956796817000053","article-title":"The calculus of dependent lambda eliminations","volume-title":"Journal of Functional Programming","author":"Stump","year":"2017"},{"key":"2026032910223726800_ref516","first-page":"149","volume-title":"Impredicative Concurrent Abstract Predicates","author":"Svendsen","year":"2014"},{"issue":"1","key":"2026032910223726800_ref517","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/2914770.2837655","article-title":"Dependent Types and Multi-monadic Effects in F*","volume":"51","author":"Swamy","year":"2016","journal-title":"SIGPLAN Not"},{"key":"2026032910223726800_ref518","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/2491956.2491978","volume-title":"PLDI","author":"Swamy","year":"2013"},{"issue":"4","key":"2026032910223726800_ref519","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1017\/S0956796808006758","article-title":"Data Types \u00e0 La Carte","volume":"18","author":"Swierstra","year":"2008","journal-title":"J. Funct. Program"},{"key":"2026032910223726800_ref520","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-03359-9_30","volume-title":"TPHOLs","author":"Swierstra","year":"2009"},{"key":"2026032910223726800_ref521","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-60275-5_74","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"Syme","year":"1995"},{"key":"2026032910223726800_ref522","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3236787","volume-title":"Equivalences for Free: Univalent Parametricity for Effective Transport","author":"Tabareau","year":"2018"},{"key":"2026032910223726800_ref523","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2816707.2816710","volume-title":"Gradual Certified Programming in Coq","author":"Tanter","year":"2015"},{"key":"2026032910223726800_ref524","first-page":"261","article-title":"Der Wahrheitsbegriff in den Formalisierten Sprachen","volume":"1","author":"Tarski","year":"1936","journal-title":"Studia Philosophica"},{"key":"2026032910223726800_ref525","first-page":"26","article-title":"Computer Assisted Reasoning with Mizar","volume":"85","author":"Trybulec","year":"1985","journal-title":"IJCAI"},{"key":"2026032910223726800_ref526","first-page":"67","volume-title":"Checking a large routine","author":"Turing","year":"1949"},{"key":"2026032910223726800_ref527","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Univalent Foundations Program","year":"2013"},{"issue":"4","key":"2026032910223726800_ref528","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","article-title":"Nominal Techniques in Isabelle\/HOL","volume":"40","author":"Urban","year":"2008","journal-title":"Journal of Automated Reasoning"},{"key":"2026032910223726800_ref529","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/978-3-642-19718-5_25","volume-title":"Programming Languages and Systems","author":"Urban","year":"2011"},{"key":"2026032910223726800_ref530","unstructured":"Valbuena, I. L. and M.Johansson. 2015. \u201cConditional Lemma Discovery and Recursion Induction in Hipster\u201d. ECEASST. 72. URL: http:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/1009."},{"key":"2026032910223726800_ref531","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-41582-1_10","volume-title":"Engineering proof by reflection in Agda","author":"Van Der Walt","year":"2012"},{"key":"2026032910223726800_ref532","unstructured":"\u201cVerified cryptography for Firefox 57\u201d. URL: https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/verified-cryptography-firefox-57."},{"issue":"5","key":"2026032910223726800_ref533","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1017\/S0960129514000577","article-title":"An experimental library of formalized Mathematics based on the univalent foundations","volume":"25","author":"Voevodsky","year":"2015","journal-title":"Mathematical Structures in Computer Science"},{"key":"2026032910223726800_ref534","unstructured":"Voevodsky, V., B.Ahrens, D.Grayson, et al.\n          2011-2019. \u201cUniMath: Univalent Mathematics\u201d. URL: https:\/\/github.com\/UniMath."},{"issue":"4","key":"2026032910223726800_ref535","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/85.238389","article-title":"First Draft of a Report on the EDVAC","volume":"15","author":"von Neumann","year":"1993","journal-title":"IEEE Ann. Hist. Comput"},{"key":"2026032910223726800_ref536","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-1-4471-3240-0_7","volume-title":"Program Refinement by Theorem Prover","author":"von Wright","year":"1994"},{"key":"2026032910223726800_ref537","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/75277.75283","volume-title":"How to Make Ad-hoc Polymorphism Less Ad Hoc","author":"Wadler","year":"1989"},{"key":"2026032910223726800_ref538","first-page":"2786","volume-title":"Advances in Neural Information Processing Systems 30","author":"Wang","year":"2017"},{"key":"2026032910223726800_ref539","volume-title":"Masterminds of Programming: Conversations with the Creators of Major Programming Languages","author":"Warden","year":"2009"},{"key":"2026032910223726800_ref540","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/3167082","volume-title":"Mechanising and verifying the WebAssembly specification","author":"Watt","year":"2018"},{"key":"2026032910223726800_ref541","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/2034773.2034818","volume-title":"Binders unbound","author":"Weirich","year":"2011"},{"key":"2026032910223726800_ref542","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11812289_3","volume-title":"Mathematical Knowledge Management","author":"Wenzel","year":"2006"},{"issue":"23","key":"2026032910223726800_ref543","first-page":"277","article-title":"Isabelle\/Isar-a generic framework for human-readable proof documents","volume":"10","author":"Wenzel","year":"2007","journal-title":"From Insight to Proof-Festschrift in Honour of Andrzej Trybulec"},{"key":"2026032910223726800_ref544","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-642-31374-5_38","volume-title":"Intelligent Computer Mathematics","author":"Wenzel","year":"2012"},{"key":"2026032910223726800_ref545","article-title":"PIDE as front-end technology for Coq","volume-title":"CoRR","author":"Wenzel","year":"2013"},{"key":"2026032910223726800_ref546","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-39634-2_30","volume-title":"Shared-Memory Multiprocessing for Interactive Theorem Proving","author":"Wenzel","year":"2013"},{"key":"2026032910223726800_ref547","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-319-08970-6_33","volume-title":"Asynchronous User Interaction and Tool Integration in Isabelle\/PIDE","author":"Wenzel","year":"2014"},{"key":"2026032910223726800_ref548","volume-title":"All about Proofs, Proofs for All","author":"Wenzel","year":"2015"},{"key":"2026032910223726800_ref549","unstructured":"Wenzel, M.\n          \n          2017a. \u201cFuture Prospects of Isabelle Technology\u201d. url: http:\/\/sketis.net\/wp-content\/uploads\/2017\/11\/Copenhagen2017.pdf."},{"key":"2026032910223726800_ref550","unstructured":"Wenzel, M.\n          \n          2017b. \u201cScaling Isabelle Proof Document Processing\u201d. url: http:\/\/sketis.net\/wp-content\/uploads\/2017\/12\/Isabelle_Scaling_Dec-2017.pdf."},{"key":"2026032910223726800_ref551","unstructured":"Wenzel, M.\n          \n          2017c. \u201cVisual Studio Code as Prover IDE for Isabelle\u201d. url: https:\/\/sketis.net\/2017\/visual-studio-code-as-prover-ide-for-isabelle."},{"key":"2026032910223726800_ref552","author":"Wenzel","year":"2018"},{"key":"2026032910223726800_ref553","unstructured":"Wenzel, M.\n          \n          2018b. \u201cIsabelle\/jEdit\u201d. url: http:\/\/isabelle.in.tum.de\/dist\/doc\/jedit.pdf."},{"key":"2026032910223726800_ref554","volume-title":"The Isabelle\/Isar reference manual","author":"Wenzel","year":"2004"},{"key":"2026032910223726800_ref555","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511623585","volume-title":"Principia mathematica to *56","author":"Whitehead","year":"1997"},{"key":"2026032910223726800_ref556","volume-title":"Refactoring proofs","author":"Whiteside","year":"2013"},{"key":"2026032910223726800_ref557","volume-title":"MA thesis","author":"Wibergh","year":"2019"},{"key":"2026032910223726800_ref558","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-44755-5_26","volume-title":"Mizar light for HOL Light","author":"Wiedijk","year":"2001"},{"key":"2026032910223726800_ref559","doi-asserted-by":"publisher","DOI":"10.1007\/11542384","volume-title":"The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science \/ Lecture Notes in Artificial Intelligence)","author":"Wiedijk","year":"2006"},{"issue":"31","key":"2026032910223726800_ref560","first-page":"137","article-title":"Statistics on digital libraries of mathematics","volume":"18","author":"Wiedijk","year":"2009","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"key":"2026032910223726800_ref561","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.entcs.2012.06.008","article-title":"Pollack-inconsistency","volume":"285","author":"Wiedijk","year":"2012","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2026032910223726800_ref562","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/2737924.2737958","volume-title":"Verdi: A Framework for Implementing and Formally Verifying Distributed Systems","author":"Wilcox","year":"2015"},{"key":"2026032910223726800_ref563","doi-asserted-by":"publisher","first-page":"1524","DOI":"10.1145\/2633628.2633631","volume-title":"Ornaments in Practice","author":"Williams","year":"2014"},{"key":"2026032910223726800_ref564","volume-title":"Inductive Proof Automation for Coq","author":"Wilson","year":"2010"},{"key":"2026032910223726800_ref565","first-page":"61","volume-title":"Verified Model Checking of Timed Automata","author":"Wimmer","year":"2018"},{"issue":"4","key":"2026032910223726800_ref566","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","article-title":"Program Development by Stepwise Refinement","volume":"14","author":"Wirth","year":"1971","journal-title":"Commun. ACM"},{"key":"2026032910223726800_ref567","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1145\/2854065.2854081","volume-title":"Planning for Change in a Formal Verification of the Raft Consensus Protocol","author":"Woos","year":"2016"},{"key":"2026032910223726800_ref568","volume-title":"Learning to Prove Theorems via Interacting with Proof Assistants","author":"Yang","year":"2019"},{"key":"2026032910223726800_ref569","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1145\/1993498.1993532","volume-title":"Finding and Understanding Bugs in C Compilers","author":"Yang","year":"2011"},{"issue":"6","key":"2026032910223726800_ref570","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1017\/S0956796806006149","article-title":"Educational Pearl: Proof-directed debugging revisited for a first-order version","volume":"16","author":"Yi","year":"2006","journal-title":"J. Funct. Program"},{"key":"2026032910223726800_ref571","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/1016850.1016875","volume-title":"Verification of safety properties for concurrent assembly code","author":"Yu","year":"2004"},{"key":"2026032910223726800_ref572","unstructured":"Z3 Development Team\n          . 2008-2019. \u201cZ3\u201d. url: http:\/\/github.com\/Z3Prover\/z3\/wiki."},{"key":"2026032910223726800_ref573","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Zalta","year":"2018"},{"key":"2026032910223726800_ref574","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Zalta","year":"2018"},{"key":"2026032910223726800_ref575","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-662-43613-4_3","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"Zeller","year":"2014"},{"key":"2026032910223726800_ref576","article-title":"AUTO2, a saturation-based heuristic prover for higherorder logic","volume-title":"CoRR","author":"Zhan","year":"2016"},{"key":"2026032910223726800_ref577","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/ICSSP.2012.6225979","volume-title":"Simulation Modeling of A Large Scale Formal Verification Process","author":"Zhang","year":"2012"},{"key":"2026032910223726800_ref578","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/2103656.2103709","volume-title":"Formalizing the LLVM intermediate representation for verified program transformations","author":"Zhao","year":"2012"},{"key":"2026032910223726800_ref579","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1017\/S0956796815000118","article-title":"Mtac: A monad for typed tactic programming in Coq","volume-title":"Journal of Functional Programming","author":"Ziliani","year":"2015"},{"key":"2026032910223726800_ref580","article-title":"Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant","volume-title":"CoRR","author":"Zimmermann","year":"2015"},{"key":"2026032910223726800_ref581","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0049-237X(08)70202-7","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Zucker","year":"1994"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/5\/2-3\/102\/11025640\/2500000045en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/5\/2-3\/102\/11025640\/2500000045en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:16:48Z","timestamp":1777486608000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/5\/2-3\/102\/1326570\/QED-at-Large-A-Survey-of-Engineering-of-Formally"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,3]]},"references-count":581,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2019,9,3]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000045","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,3]]}}}