Stream: Miscellaneous

Topic: Extraction of interaction trees


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Li-yao (Dec 02 2022 at 12:59):

Something similar would probably work on itrees.

view this post on Zulip 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: Jan 29 2023 at 18:03 UTC