erwanm974 / coq_interaction_semantics_equivalence_with_coregions Goto Github PK
View Code? Open in Web Editor NEWFormal proof of the equivalence of a denotational and operational semantics for an interaction language with a concurrent region primitive which covers both interleaving and weak sequencing.
License: Apache License 2.0