I seem to recall work on (efficient) extraction of interaction trees, but it does not seem to show up here:
Am I misremembering?
There's nothing on doing it efficiently yet. But you can look at what FreeSpec does about extraction.
We haven't even done any proper evaluation as to _how_ slow it is by default. It scales reasonably for testing purpose from what we observe in Vellvm, but we really should look into this more properly
@Li-yao Thanks. Are you saying that FreeSpec is using ITrees, or just that something similar to FreeSpec might work for ITrees?
Something similar would probably work on itrees.
We plan to also look at this in the context of CertiCoq (and VeriFFI I guess), but we only have a naive and unverified treatment of coinductives for now.
Last updated: May 31 2023 at 02:31 UTC