Iris on Indirection Theory: Lightweight Higher-order Ghost State
Darius Foo, Viet-Anh Nguyen, Wei-Ngan Chin
cs.PL
Oct 30, 2026 · v1
TL;DR
Mechanises Indirection Theory in Lean with Iris-style resource algebra functors, reconstructs the Iris base logic, and builds logical relations and a program logic.
Abstract
Today, semantic models of languages with concurrency and higher-order state are constructed using step-indexed predicates over resources and higher-order ghost state. There are two main lines of work for constructing such models. On the one hand, Iris provides these in full generality, at the cost of a large body of mechanised domain theory that is difficult to learn and port to new proof assistants. On the other hand, Indirection Theory is much simpler through the use of ordinary dependent types, but its foundation in separation algebra limits the expressiveness of its resource model compared to Iris-style higher-order ghost state. We resolve this conundrum by showing that Indirection Theory can be as expressive as Iris. To that end, we give a lightweight mechanisation of Indirection Theory in Lean, generalised so knots contain resources from an Iris-style resource algebra functor. We then reconstruct the Iris base logic on top of it. The advantage of this approach is in the elementary metatheory: a user can follow the whole construction without domain theory. We conduct two case studies to show that the base logic is expressive and faithful to Iris: a biorthogonal logical relation for higher-order state, and an Iris-style program logic with invariants and user-definable ghost state, complete enough to verify concurrent and higher-order programs.
Problem
Semantic models for languages with concurrency and higher-order state need step-indexed predicates and higher-order ghost state. Iris provides these through a large body of domain theory that is hard to learn and to port to other proof assistants. Indirection Theory is simpler, but its separation-algebra foundation gives it a less expressive resource model than Iris.
Approach
The authors give a lightweight Lean mechanisation of Indirection Theory, generalised so that knots carry resources from an Iris-style resource algebra functor. It is built in layers: resources, knots, hereditary predicates, and logical connectives, with Löb induction and guarded recursion. The Iris base logic is then reconstructed on top using only dependent types. Proofs use Lean tactics for entailment rewriting, frame inference, and biabduction.
Results
Two case studies show the base logic is expressive and faithful to Iris. The first is a biorthogonal logical relation for a stateful lambda calculus. The second is an Iris-style program logic for HeapLang with invariants and user-definable ghost state, complete enough to verify concurrent and higher-order programs.
