Machine-checked semantic session typing

Session types- A family of type systems for message-passing concurrency-have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine checked, making their correctness less trustworthy. We overcome...