Sciweavers

Share
TLDI
2009
ACM

Towards type-theoretic semantics for transactional concurrency

11 years 10 months ago
Towards type-theoretic semantics for transactional concurrency
We propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design builds upon our previous work on Hoare Type Theory (HTT), which we extend with types that correspond to Hoare-style specifications for transactions. The types track shared and local state of the process separately, and enforce that shared state always satisfies a given invariant, except at specific critical sections which appear to execute atomically. Atomic sections may violate the invariant, but must restore it upon exit. HTT follows Separation Logic in providing tight specifications of space requirements. As a logic, we argue that HTT is sound and compositional. As a programming language, we define its operational semantics and show adequacy with respect to specifications. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs...
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2009
Where TLDI
Authors Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Comments (0)
books