search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
198 stars 50 forks source link

Trace #216

Closed lag47 closed 2 years ago

lag47 commented 2 years ago

One of 3 partial commits to bring the secure branch into master. This branch adds the ITraces, a linear, coinductive trace data type built on top of ITrees. ITraces are implemented as ITrees over a specialized event type family. This branch introduces a trace refinement relation, creating a trace model for ITrees that is proven sound and complete over eutt.

(Note that the Coq 8.13 + make build is breaking on this pull request. However, the dijkstra_pull_request and secure branches do not have this problem, so it is probably not worth tracking down)

Lysxia commented 2 years ago

This looks good to me! Just a few comments above to address, and I need to update the documentation about axioms.

Lysxia commented 2 years ago

I also moved eutt_div, must_diverge and can_converge into Props.EuttDiv and Props.Divergence since they can be defined without reference to traces.