Document Open Access Logo

A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Author Joshua M. Cohen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.5.pdf
  • Filesize: 0.91 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.5.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
  • Theory of computation → Logic and verification
Keywords
  • Pattern Matching Compilation
  • Algebraic Data Types
  • First-Order Logic

Metrics

Abstract

Algebraic data types (ADTs) and pattern matching are widely used to write elegant functional programs and to specify program behavior. These constructs are critical to most general-purpose interactive theorem provers (e.g. Lean, Rocq/Coq), first-order SMT-based deductive verifiers (e.g. Dafny, VeriFast), and intermediate verification languages (e.g. Why3). Such features require layers of compilation - in Rocq, pattern matches are compiled to remove nesting, while SMT-based tools further axiomatize ADTs with a first-order specification. However, these critical steps have been omitted from prior formalizations of such toolchains (e.g. MetaRocq). We give the first proved-sound sophisticated pattern matching compiler (based on Maranget’s compilation to decision trees) and first-order axiomatization of ADTs, both based on Why3 implementations. We prove the soundness of exhaustiveness checking, extending pen-and-paper proofs from the literature, and formulate a robustness property with which we find an exhaustiveness-related bug in Why3. We show that many of our proofs could be useful for reasoning about any first-order program verifier supporting ADTs.

Cite As Get BibTex

Joshua M. Cohen. A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.5

Author Details

Joshua M. Cohen
  • Princeton University, NJ, USA

Funding

This research was supported in part by National Science Foundation grant CCF-2219757.

Acknowledgements

I would like to thank Philip Johnson-Freyd, Andrew W. Appel, and the anonymous reviewers for their suggestions and feedback.

Supplementary Materials

References

  1. Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. CertiCoq: A Verified Compiler for Coq. In CoqPL'17: The Third International Workshop on Coq for Programming Languages, Paris, France, January 2017. Google Scholar
  2. Andrew W. Appel. Program Logics for Certified Compilers. Cambridge University Press, Cambridge, 2014. URL: https://doi.org/10.1017/CBO9781107256552.
  3. Andrew W. Appel. Verification of a Cryptographic Primitive: SHA-256. ACM Transactions on Programming Languages and Systems (TOPLAS), 37(2):7:1-7:31, April 2015. URL: https://doi.org/10.1145/2701415.
  4. Lennart Augustsson. Compiling Pattern Matching. In Jean-Pierre Jouannaud, editor, Functional Programming Languages and Computer Architecture, pages 368-381, Nancy, France, 1985. Springer. URL: https://doi.org/10.1007/3-540-15975-4_48.
  5. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects, pages 364-387, Amsterdam, Netherlands, 2006. Springer. URL: https://doi.org/10.1007/11804192_17.
  6. Clark Barrett, Igor Shikanian, and Cesare Tinelli. An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. Electronic Notes in Theoretical Computer Science, 174(8):23-37, June 2007. URL: https://doi.org/10.1016/j.entcs.2006.11.037.
  7. Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. EasyCrypt: A Tutorial. In Alessandro Aldini, Javier Lopez, and Fabio Martinelli, editors, Foundations of Security Analysis and Design VII: FOSAD 2012/2013 Tutorial Lectures, pages 146-166. Springer International Publishing, Bertinoro, Italy, 2014. URL: https://doi.org/10.1007/978-3-319-10082-1_6.
  8. Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial. Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 63-77, Boston, USA, January 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575676.
  9. Valentin Blot, Louise Dubois de Prisque, Chantal Keller, and Pierre Vial. General Automation in Coq through Modular Transformations. In Proceedings of the Seventh Workshop on Proof eXchange for Theorem Proving, Pittsburgh, United States, July 2021. URL: https://doi.org/10.4204/EPTCS.336.3.
  10. François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, page 53, Wrocław, Poland, 2011. Google Scholar
  11. Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clement Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, and Yongwei Yuan. Formally Verified Cloud-Scale Authorization. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 2508-2521, Ottawa, Canada, April 2025. IEEE Computer Society. URL: https://doi.org/10.1109/ICSE55347.2025.00166.
  12. Joshua M. Cohen. Proof Artifact for "A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching". Software, (visited on 2025-09-08). URL: https://github.com/joscoh/why3-semantics/tree/itp25
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24696
  13. Joshua M. Cohen. A Foundationally Verified Intermediate Verification Language. PhD thesis, Princeton University, United States - New Jersey, 2025. Google Scholar
  14. Joshua M. Cohen and Philip Johnson-Freyd. A Formalization of Core Why3 in Coq. Proceedings of the ACM on Programming Languages, 8(POPL):60:1789-60:1818, January 2024. URL: https://doi.org/10.1145/3632902.
  15. Joshua M. Cohen, Qinshi Wang, and Andrew W. Appel. Verified Erasure Correction in Coq with MathComp and VST. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification, pages 272-292, Haifa, Israel, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-13188-2_14.
  16. Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. Formal Foundations for Translational Separation Logic Verifiers. Proceedings of the ACM on Programming Languages, 9(POPL):20:569-20:599, January 2025. URL: https://doi.org/10.1145/3704856.
  17. Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Adrian Riesco and Min Zhang, editors, Formal Methods and Software Engineering, pages 90-105, Berlin, Germany, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-17244-1_6.
  18. Jean-Christophe Filliâtre. One Logic to Use Them All. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24, pages 1-20, Lake Placid, New York, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-38574-2_1.
  19. Quentin Garchery. A Framework for Proof-carrying Logical Transformations. In Proceedings of the Seventh Workshop on Proof eXchange for Theorem Proving, volume 336, pages 5-23, Pittsburgh, United States, July 2021. URL: https://doi.org/10.4204/EPTCS.336.2.
  20. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet: Proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles, pages 1-17, Monterey, California, USA, October 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2815400.2815428.
  21. Paolo Herms. Certification of a Tool Chain for Deductive Program Verification. PhD thesis, Université Paris Sud - Paris XI, January 2013. Google Scholar
  22. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, pages 41-55, Pasadena, California, USA, 2011. Springer. URL: https://doi.org/10.1007/978-3-642-20398-5_4.
  23. Bart Jacobs, Frédéric Vogels, and Frank Piessens. Featherweight VeriFast. Logical Methods in Computer Science, Volume 11, Issue 3, September 2015. URL: https://doi.org/10.2168/LMCS-11(3:19)2015.
  24. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. Formal Aspects of Computing, 27(3):573-609, May 2015. URL: https://doi.org/10.1007/s00165-014-0326-7.
  25. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. ACM SIGPLAN Notices, 49(1):179-191, January 2014. URL: https://doi.org/10.1145/2578855.2535841.
  26. Alain Laville. Implementation of lazy pattern matching algorithms. In H. Ganzinger, editor, ESOP '88, pages 298-316, Nancy, France, 1988. Springer. URL: https://doi.org/10.1007/3-540-19027-9_20.
  27. Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, pages 26-37, Florence, Italy, October 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/507635.507641.
  28. K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 348-370, Dakar, Senegal, 2010. Springer. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  29. Alessandro Maissen. Adding Algebraic Data Types to a Verification Language. Technical report, ETH Zurich, April 2022. Google Scholar
  30. Luc Maranget. Compiling lazy pattern matching. In Proceedings of the 1992 ACM Conference on LISP and Functional Programming, LFP '92, pages 21-31, San Francisco, USA, January 1992. Association for Computing Machinery. URL: https://doi.org/10.1145/141471.141499.
  31. Luc Maranget. Warnings for pattern matching. Journal of Functional Programming, 17(3):387-421, May 2007. URL: https://doi.org/10.1017/S0956796807006223.
  32. Luc Maranget. Compiling pattern matching to good decision trees. In Proceedings of the 2008 ACM SIGPLAN Workshop on ML, ML '08, pages 35-46, Victoria, British Columbia, Canada, September 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1411304.1411311.
  33. Per Martin-Löf. Constructive Mathematics and Computer Programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors, Studies in Logic and the Foundations of Mathematics, volume 104 of Logic, Methodology and Philosophy of Science VI, pages 153-175. Elsevier, January 1982. URL: https://doi.org/10.1016/S0049-237X(09)70189-2.
  34. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation, pages 41-62, St Petersburg, Florida, USA, 2016. Springer. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  35. Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, and Alexander J. Summers. Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. Proceedings of the ACM on Programming Languages, 8(PLDI):208:1510-208:1534, June 2024. URL: https://doi.org/10.1145/3656438.
  36. Gaurav Parthasarathy, Peter Müller, and Alexander J. Summers. Formally Validating a Practical Verification Condition Generator. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 704-727. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_33.
  37. João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, and Adrian Perrig. Protocols to Code: Formal Verification of a Next-Generation Internet Router, May 2024. URL: https://doi.org/10.48550/arXiv.2405.06074.
  38. Amar Shah, Federico Mora, and Sanjit A. Seshia. An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes. Proceedings of the AAAI Conference on Artificial Intelligence, 38(8):8099-8107, March 2024. URL: https://doi.org/10.1609/aaai.v38i8.28649.
  39. Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Nielsen, Nicolas Tabareau, and Théo Winterhalter. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. Journal of the ACM, 72(1):8:1-8:74, January 2025. URL: https://doi.org/10.1145/3706056.
  40. Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in Coq. Proceedings of the ACM on Programming Languages, 3(ICFP):86:1-86:29, July 2019. URL: https://doi.org/10.1145/3341690.
  41. Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, and Jean-Baptiste Jeannin. Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. In Intelligent Computer Mathematics: 16th International Conference, CICM 2023, pages 206-221, Cambridge, UK, September 2023. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-42753-4_14.
  42. Thomas Tuerk, Magnus O. Myreen, and Ramana Kumar. Pattern Matches in HOL:. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, pages 453-468, Nanjing, China, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-22102-1_30.
  43. Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, and Peter Müller. Gobra: Modular Specification and Verification of Go Programs. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 367-379. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_17.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact