vellvm / ctrees

An itree-like data-structure to additionally support internal non-determinism
MIT License
13 stars 2 forks source link

Meta-theory for refinements/simulations #6

Closed YaZko closed 2 years ago

YaZko commented 2 years ago

The current bisimulations are already cleanly defined in terms of a symetrized simulation endofunction, but we do not currently define the gfp of the latter.

TODO: define and develop the meta-theory for simulations.

nchappe commented 2 years ago

I think #17 closes this issue.