Soundness Proof of Order Types in Coq

This page makes the Coq formalization for soundness of order types available.

• syntax.v defines the program syntax for an asynchronous message passing core calculus as well as the syntax for order types.
• static_semantics.v defines the inference and closure of order types in the core calculus.
• configurations.v defines the configuration and dynamic objects used in dynamic semantics.
• dynamic_semantics.v defines the dynamic semantics of the core calculus.
• soundness.v defines and proves the soundness of order types.
• auxiliary_functions.v defines the auxiliary functions used in the static and dynamic semantics and proofs.

The entirity of the formalization is also available via this ZIP archive.