Skip to content

WIP: step_proto abstraction

Jonas Kastberg requested to merge step_proto into master

This merge request hides the multiple laters that arise from using the Actris Ghost Theory, via a "step-taking" modality |~~> P, that captures the obligation to take a step of the operational semantics.

One motivation for this is being able to present the abstraction in a way that requires less explanation.

The MR depends on the following outstanding MR of the Iris development iris!887

Merge request reports