Sponsor
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.
Published In
Schloss Dagstuhl–Leibniz-Zentrum für Informatik
Document Type
Article
Publication Date
10-2026
Subjects
Computer science
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., 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.
Rights
Copyright (c) 2026 The Authors
This work is licensed under a Creative Commons Attribution 4.0 International License.
Locate the Document
https://doi.org/10.4230/LIPIcs.ITP.2026.16
DOI
10.4230/LIPIcs.ITP.2026.16
Citation Details
Lin, Y., Kariniemi, I., & Li, Y. (2026). Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees. In 17th International Conference on Interactive Theorem Proving (ITP 2026) (pp. 16-1). Schloss Dagstuhl–Leibniz-Zentrum für Informatik.