Bas Spitters (Dec 01 2022 at 12:22): Bas Spitters (Dec 01 2022 at 12:22):I seem to recall work on (efficient) extraction of interaction trees, but it does not seem to show up here:
https://github.com/DeepSpec/InteractionTrees
Am I misremembering?
Li-yao (Dec 01 2022 at 13:38):There's nothing on doing it efficiently yet. But you can look at what FreeSpec does about extraction.
Yannick Zakowski (Dec 01 2022 at 16:01):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
Bas Spitters (Dec 02 2022 at 08:42):@Li-yao Thanks. Are you saying that FreeSpec is using ITrees, or just that something similar to FreeSpec might work for ITrees?
Li-yao (Dec 02 2022 at 12:59):Something similar would probably work on itrees.
Matthieu Sozeau (Dec 07 2022 at 16:59):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