Towards Type-Theoretic Semantics for Transactional Concurrency
View/ Open
Nanevski_Towards.pdf (252.6Kb)
Access Status
Full text of the requested work is not available in DASH at this time ("restricted access"). For more information on restricted deposits, see our FAQ.Published Version
https://doi.org/10.1145/1481861.1481872Metadata
Show full item recordCitation
Nanevski, Aleksandar, Paul Govereau, and Greg Morrisett. 2009. Towards type-theoretic semantics for transactional concurrency. In Proceedings of the 4th International Workshop on Types in Languages Design and Implementation: January 24, 2009, Savannah, GA, ed. A. Kennedy, 79-90. New York, N.Y.: ACM Press.Abstract
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.
Other Sources
http://ynot.cs.harvard.edu/papers/tldi09.pdfCitable link to this page
http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980867
Collections
- FAS Scholarly Articles [18256]
Contact administrator regarding this item (to report mistakes or request changes)