Towards Type-Theoretic Semantics for Transactional Concurrency

DSpace/Manakin Repository

Towards Type-Theoretic Semantics for Transactional Concurrency

Citable link to this page

. . . . . .

Title: Towards Type-Theoretic Semantics for Transactional Concurrency
Author: Nanevski, Aleksandar; Govereau, Paul; Morrisett, John Gregory

Note: Order does not necessarily reflect citation order of authors.

Citation: 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.
Access Status: At the direction of the depositing author this work is not currently accessible through DASH.
Full Text & Related Files:
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.
Published Version: http://portal.acm.org/citation.cfm?id=1481861.1481872
Other Sources: http://ynot.cs.harvard.edu/papers/tldi09.pdf
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980867

Show full Dublin Core record

This item appears in the following Collection(s)

  • FAS Scholarly Articles [6463]
    Peer reviewed scholarly articles from the Faculty of Arts and Sciences of Harvard University
 
 

Search DASH


Advanced Search
 
 

Submitters