Fetching the paper…
Reading the bibliography…
Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified requirements.
Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 337–340
Leonardo De Moura and Nikolaj Bjørner. 2008 · 2008
Earlier work this paper cites.
Large-scale formal verification in practice: A process perspective. In 2012 34th International Conference on Software Engineering (ICSE) . IEEE, 1002–1011
June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, and Liming Zhu. 2012 · 2012
Earlier work this paper cites.
Productivity for proof engineering. In Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement . 1–4
Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein, and Rafal Kolanski. 2014 · 2014
Earlier work this paper cites.
Mining the archive of formal proofs. In International Conference on Intelligent Computer Mathematics . Springer, 3–17
Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. 2015 · 2015
Earlier work this paper cites.
Towards formal proof metrics. In Fundamental Approaches to Software Engineering: 19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings 19 . Springer, 325–341
David Aspinall and Cezary Kaliszyk. 2016 · 2016
Earlier work this paper cites.
Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 256–270
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016 · 2016
Earlier work this paper cites.
HACL*: A Verified Modern Cryptographic Library. In ACM Conference on Computer and Communications Security . ACM, 1789–1806
Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017 · 2017
Earlier work this paper cites.
Software Engineering: A Practitioner’s Approach (9th ed.)
Roger Pressman and Bruce Maxim. 2019 · 2019
Earlier work this paper cites.
Untangling mechanized proofs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (Virtual, USA) (SLE 2020) . Association for Computing Machinery, New York, NY, USA, 155–174
Clément Pit-Claudel. 2020 · 2020
Earlier work this paper cites.
REPLica: REPL instrumentation for Coq analysis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs . 99–113
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. 2020 · 2020
Earlier work this paper cites.
Program synthesis with large language models
Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al · 2021
Cited alongside, same era.
A Data-Centered User Study for Proof Assistant Tools.. In PPIG
Hanneli CA Tavante. 2021 · 2021
Cited alongside, same era.
Hardening attack surfaces with formally proven binary format parsers. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (San Diego, CA, USA) (PLDI 2022) . Association for Computing Machinery, New York, NY, USA, 31–45
Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta. 2022 · 2022
Cited alongside, same era.
Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (San Francisco, CA, USA) (ESEC/FSE 2023) . Association for Computing Machinery, New York, NY, USA, 1229–1241
Lean-star: Learning to interleave thinking and proving
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. 2024 · 2024
Later among the works it cites.
Thirty-Three Years of Mathematicians and Software Engineers: A Case Study of Domain Expertise and Participation in Proof Assistant Ecosystems. In 2024 IEEE/ACM 21st International Conference on Mining Software Repositories (MSR) . IEEE, 1–13
Gwenyth Lincroft, Minsung Cho, Katherine Hough, Mahsa Bazzaz, and Jonathan Bell. 2024 · 2024
Later among the works it cites.
The landscape of emerging ai agent architectures for reasoning, planning, and tool calling: A survey
Tula Masterman, Sandi Besen, Mason Sawtell, and Alex Chao. 2024 · 2024
Later among the works it cites.
Towards AI-Assisted Synthesis of Verified Dafny Methods
Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024 · 2024
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023 · 2023
Cited alongside, same era.
Verifying Indistinguishability of Privacy-Preserving Protocols
Kirby Linvill, Gowtham Kaki, and Eric Wustrow. 2023 · 2023
Cited alongside, same era.
Proof-oriented programming for high-assurance systems. In Proceedings of the 16th Innovations in Software Engineering Conference (Allahabad, India) (ISEC ’23) . Association for Computing Machinery, New York, NY, USA, Article 3, 1 pages
Aseem Rastogi. 2023 · 2023
Cited alongside, same era.
LLMSTEP: LLM proofstep suggestions in Lean
Sean Welleck and Rahul Saha. 2023 · 2023
Cited alongside, same era.
Pranjal Aggarwal, Bryan Parno, and Sean Welleck. 2024 · 2024
Cited alongside, same era.
From local to global: A graph rag approach to query-focused summarization
Darren Edge, Ha Trinh, Newman Cheng, Joshua Bradley, Alex Chao, Apurva Mody, Steven Truitt, Dasha Metropolitansky, Robert Osazuwa Ness, and Jonathan Larson. 2024 · 2024
Cited alongside, same era.
Verus: A Practical Foundation for Systems Verification. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024 . ACM, 438–454
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024 · 2024
Cited alongside, same era.
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. 2024 · 2024
Later among the works it cites.
Autogen: Enabling next-gen LLM applications via multi-agent conversations. In First Conference on Language Modeling
Qingyun Wu, Gagan Bansal, Jieyu Zhang, Yiran Wu, Beibin Li, Erkang Zhu, Li Jiang, Xiaoyun Zhang, Shaokun Zhang, Jiale Liu, et al · 2024
Later among the works it cites.
Towards Neural Synthesis for SMT-assisted Proof-Oriented Programming . In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE) . IEEE Computer Society, Los Alamitos, CA, USA, 13–25
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy. 2025 · 2025
Closest in time.
OpenAI o3 (reasoning large language model)
OpenAI. 2025 · 2025
Closest in time.
QED in Context: An Observation Study of Proof Assistant Users
Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C Pierce, and Andrew Head. 2025 · 2025
Closest in time.