1 paper
David Nowak, Vlad Rusu
We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we…