Machine-checked semantic session typing

Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

19 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationCPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021
EditorsCatalin Hritcu, Andrei Popescu
PublisherAssociation for Computing Machinery (ACM)
Pages178-198
Number of pages21
ISBN (Electronic)9781450382991
DOIs
Publication statusPublished - 2021
Event10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 - Virtual, Online, Denmark
Duration: 17 Jan 202119 Jan 2021

Publication series

NameCPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021

Conference

Conference10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021
CountryDenmark
CityVirtual, Online
Period17/01/2119/01/21

Keywords

  • Concurrency
  • Coq
  • Iris
  • Message passing
  • Semantic typing
  • Separation logic
  • Session types

Fingerprint

Dive into the research topics of 'Machine-checked semantic session typing'. Together they form a unique fingerprint.

Cite this