Document Open Access Logo

Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees

Authors Yiming Lin , Ian Kariniemi , Yao Li

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.16.pdf
  • Filesize: 0.85 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
  • Software and its engineering → Software verification
Keywords
  • interaction trees
  • formal verification
  • metaprogramming

Metrics

Abstract

Verifying existing software is hard: Programs are developed in languages not amenable to verification, involve complicated optimizations that obscure the underlying logic, and are gigantic in size. In this paper, we propose a way to ease this pain via a simplification framework that employs interaction trees as a language-agnostic interface. We show that local variable lifting, the technique underlying AutoCorres for the Simpl language, can be generalized to interaction trees via an implementation in Rocq. A key challenge with simplifying interaction trees is that they are highly dynamic structures and we would like our approach to work with mostly uninterpreted trees. We address this challenge via metaprogramming. Our metaprogramming framework is semi-automatic and proof-guided, i.e.ie we obtain the simplified code via a constructive proof of equivalence that can be automated via proof tactics, by utilizing Rocq’s Derive extension. This approach gives us simplified code and the equivalence theorem in one step. We demonstrate that our approach is practical using examples inspired by real-world applications.

Cite As Get BibTex

Yiming Lin, Ian Kariniemi, and Yao Li. Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.16

Author Details

Yiming Lin
  • Portland State University, OR, USA
Ian Kariniemi
  • Portland State University, OR, USA
Yao Li
  • Portland State University, OR, USA

Funding

This work was partially supported by the National Science Foundation under Grant No. CCF-2348490. Ian Kariniemi was partially funded by Bloomberg L.P. as a Fellow in the Bloomberg Infrastructure & Security Ph.D. Fellowship Program.

Acknowledgements

We thank all anonymous reviewers of ITP'26, whose feedback has helped greatly improve this paper. We thank Mike Dodds, Mark P. Jones, Andrew Tolmach, and Fei Xie for their feedback to this work, and Alex Hodges and Allison Naaktgeboren for their feedback to this paper.

Supplementary Materials

References

  1. Jirí Adámek, Stefan Milius, and Jirí Velebil. Elgot theories: a new perspective on the equational properties of iteration. Math. Struct. Comput. Sci., 21(2):417-480, 2011. URL: https://doi.org/10.1017/S0960129510000496.
  2. Andrew W. Appel. SSA is functional programming. ACM SIGPLAN Notices, 33(4):17-20, 1998. URL: https://doi.org/10.1145/278283.278285.
  3. Andrew W. Appel. Program Logics for Certified Compilers. Cambridge University Press, United States, 2014. URL: https://doi.org/10.1017/CBO9781107256552.
  4. Sandrine Blazy and Xavier Leroy. Mechanized semantics for the clight subset of the C language. CoRR, abs/0901.3619, 2009. URL: https://doi.org/10.48550/arXiv.0901.3619.
  5. Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch, and Simon Wimmer. AutoCorres2. Arch. Formal Proofs, 2024. URL: https://www.isa-afp.org/entries/AutoCorres2.html.
  6. Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen, and Stephanie Weirich. Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. J. Funct. Program., 31:e5, 2021. URL: https://doi.org/10.1017/S0956796820000283.
  7. Adam Chlipala. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013. URL: http://mitpress.mit.edu/books/certified-programming-dependent-types.
  8. Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Adrián Riesco and Min Zhang, editors, Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24-27, 2022, Proceedings, volume 13478 of Lecture Notes in Computer Science, pages 90-105. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17244-1_6.
  9. Andrzej Filinski. Normalization by Evaluation for the Computational Lambda-Calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings, volume 2044 of Lecture Notes in Computer Science, pages 151-165. Springer, 2001. URL: https://doi.org/10.1007/3-540-45413-6_15.
  10. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science, pages 125-128. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_8.
  11. Formal Land development team. rocq-of-rust. URL: https://github.com/formal-land/rocq-of-rust.
  12. Jeremy Gibbons. The School of Squiggol - A History of the Bird-Meertens Formalism. In Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Creissac Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, and David Delmas, editors, Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II, volume 12233 of Lecture Notes in Computer Science, pages 35-53. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54997-8_2.
  13. Eduardo Giménez. Un calcul de constructions infinies et son application à la vérification de systèmes communicants. PhD thesis, École normale supérieure de Lyon, 1996. Thèse de doctorat dirigée par Bougé, Luc Sciences appliquées École normale supérieure de Lyon (Lyon ; 1987-2009) 1996. URL: http://www.theses.fr/1996ENSL0044.
  14. Sergey Goncharov. Shades of Iteration: From Elgot to Kleene. In Alexandre Madeira and Manuel A. Martins, editors, Recent Trends in Algebraic Development Techniques - 26th IFIP WG 1.3 International Workshop, WADT 2022, Aveiro, Portugal, June 28-30, 2022, Revised Selected Papers, volume 13710 of Lecture Notes in Computer Science, pages 100-120. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-43345-0_5.
  15. David Greenaway. Automated proof-producing abstraction of C code. PhD thesis, University of New South Wales, Sydney, Australia, 2014. URL: https://doi.org/10.26190/unsworks/17396.
  16. David Greenaway, June Andronick, and Gerwin Klein. Bridging the Gap: Automatic Verified Abstraction of C. In Lennart Beringer and Amy P. Felty, editors, Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, volume 7406 of Lecture Notes in Computer Science, pages 99-115. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_8.
  17. David Greenaway, Japheth Lim, June Andronick, and Gerwin Klein. Don't sweat the small stuff: formal verification of C code without the pain. In Michael F. P. O'Boyle and Keshav Pingali, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09-11, 2014, pages 429-439. ACM, 2014. URL: https://doi.org/10.1145/2594291.2594296.
  18. Samuel Gruetter, Viktor Fukala, and Adam Chlipala. Live Verification in an Interactive Proof Assistant. Proc. ACM Program. Lang., 8(PLDI):1535-1558, 2024. URL: https://doi.org/10.1145/3656439.
  19. Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve Zdancewic. A type system for extracting functional specifications from memory-safe imperative programs. Proc. ACM Program. Lang., 5(OOPSLA):1-29, 2021. URL: https://doi.org/10.1145/3485512.
  20. Son Ho and Jonathan Protzenko. Aeneas: Rust verification by functional translation. Proc. ACM Program. Lang., 6(ICFP):711-741, 2022. URL: https://doi.org/10.1145/3547647.
  21. Mark P. Jones. Functional programming with overloading and higher-order polymorphism. In Johan Jeuring and Erik Meijer, editors, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text, volume 925 of Lecture Notes in Computer Science, pages 97-136, Berlin, Heidelberg, 1995. Springer. URL: https://doi.org/10.1007/3-540-59451-5_4.
  22. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 94-105, 2015. URL: https://doi.org/10.1145/2804302.2804319.
  23. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang., 7(OOPSLA1):286-315, 2023. URL: https://doi.org/10.1145/3586037.
  24. William Mansky and Ke Du. An Iris Instance for Verifying CompCert C Programs. Proc. ACM Program. Lang., 8(POPL):148-174, 2024. URL: https://doi.org/10.1145/3632848.
  25. Eugenio Moggi. Notions of Computation and Monads. Inf. Comput., 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  26. Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. Refinedc: automating the foundational verification of C code with refined ownership types. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, PLDI 2021, pages 158-174, New York, NY, USA, 2021. ACM. URL: https://doi.org/10.1145/3453483.3454036.
  27. Norbert Schirmer. Verification of sequential imperative programs in Isabelle-HOL. PhD thesis, Technical University Munich, Germany, 2006. URL: http://mediatum.ub.tum.de/mediatum/servlets/TUMDistributionServlet?id=mediaTUM_derivate_000000000002972.
  28. Norbert Schirmer. A sequential imperative programming language syntax, semantics, hoare logics and verification environment. Arch. Formal Proofs, 2008, February 2008. , Formal proof development. URL: https://isa-afp.org/entries/Simpl.html.
  29. Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. Total Haskell is reasonable Coq. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 14-27. ACM, 2018. URL: https://doi.org/10.1145/3167092.
  30. Sebastian Ullrich. Simple Verification of Rust Programs via Functional Purification. Master’s thesis, Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany, December 2016. Master’s thesis, Institute for Program Structures and Data Organization (IPD). URL: https://pp.ipd.kit.edu/uploads/publikationen/ullrich16masterarbeit.pdf.
  31. Philip Wadler. Comprehending Monads. Math. Struct. Comput. Sci., 2(4):461-493, 1992. URL: https://doi.org/10.1017/S0960129500001560.
  32. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact