Print Email Facebook Twitter Machine-checked semantic session typing Title Machine-checked semantic session typing Author Hinrichsen, Jonas Kastberg (University of Copenhagen) Louwrink, Daniël (Universiteit van Amsterdam) Krebbers, R.J. (TU Delft Programming Languages; Radboud Universiteit Nijmegen) Bengtson, Jesper (University of Copenhagen) Contributor Hritcu, Catalin (editor) Popescu, Andrei (editor) Date 2021 Abstract 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 these shortcomings with a semantic approach to binary asynchronous affine session types, by developing a logical relations model in Coq using the Iris program logic. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, references, and locks/mutexes. As an additional benefit of the semantic approach, we demonstrate how to manually prove typing judgements of racy, but safe, programs that cannot be type checked using only the rules of the type system. Subject ConcurrencyCoqIrisMessage passingSemantic typingSeparation logicSession types To reference this document use: http://resolver.tudelft.nl/uuid:9e66cf2e-d6bc-4f5f-bf72-02f7c2e15e0e DOI https://doi.org/10.1145/3437992.3439914 Publisher Association for Computing Machinery (ACM) ISBN 9781450382991 Source CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021 Event 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021, 2021-01-17 → 2021-01-19, Virtual, Online, Denmark Series CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021 Part of collection Institutional Repository Document type conference paper Rights © 2021 Jonas Kastberg Hinrichsen, Daniël Louwrink, R.J. Krebbers, Jesper Bengtson Files PDF 3437992.3439914.pdf 433.12 KB Close viewer /islandora/object/uuid:9e66cf2e-d6bc-4f5f-bf72-02f7c2e15e0e/datastream/OBJ/view