uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Compositional Theory for STM Haskell
Microsoft Research, Cambridge.
Microsoft Research, Cambridge.
Microsoft Research, Cambridge.
2009 (English)In: Proceedings of the 2nd ACM SIGPLAN symposium on Haskell, ACM Press , 2009, 69-80 p.Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of reasoning about Haskell programs that use Software Transactional Memory (STM). As a motivating example, we consider Haskell code for a concurrent non-deterministic tree rewriting algorithm implementing the operational semantics of the ambient calculus. The core of our theory is a uniform model, in the spirit of process calculi, of the run-time state of multi-threaded STM Haskell programs. The model was designed to simplify both local and compositional reasoning about STM programs. A single reduction relation captures both pure functional computations and also effectful computations in the STM and I/O monads. We state and prove liveness, soundness, completeness, safety, and termination properties relating source processes and their Haskell implementation. Our proof exploits various ideas from concurrency theory, such as the bisimulation technique, but in the setting of a widely used programming language rather than an abstract process calculus. Additionally, we develop an equational theory for reasoning about STM Haskell programs, and establish for the first time equations conjectured by the designers of STM Haskell. We conclude that using a pure functional language extended with STM facilitates reasoning about concurrent implementation code. 

Place, publisher, year, edition, pages
ACM Press , 2009. 69-80 p.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-161493DOI: 10.1145/1596638.1596648ISBN: 978-1-60558-508-6 (print)OAI: oai:DiVA.org:uu-161493DiVA: diva2:456314
Conference
Haskell’09
Available from: 2011-11-14 Created: 2011-11-14

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Borgström, Johannes

Search in DiVA

By author/editor
Borgström, Johannes
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 366 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf