DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.16

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

Authors: Yiming Lin, Ian Kariniemi, and Yao Li

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{lin_et_al:LIPIcs.ITP.2026.16,
  author =	{Lin, Yiming and Kariniemi, Ian and Li, Yao},
  title =	{{Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.16},
  URN =		{urn:nbn:de:0030-drops-269903},
  doi =		{10.4230/LIPIcs.ITP.2026.16},
  annote =	{Keywords: interaction trees, formal verification, metaprogramming}
}

Search Results

Documents authored by Kariniemi, Ian

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

Abstract

Cite as

Thanks for your feedback!

Could not send message