Towards Type-Theoretic Semantics for Transactional Concurrency

The authors propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design builds upon their previous work on Hoare Type Theory (HTT), which they 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.