Correctness of an STM Haskell implementation
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of con icting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.
| Author: | Manfred Schmidt-Schauß, David Sabel |
|---|---|
| URN: | urn:nbn:de:hebis:30:3-270077 |
| Series (Serial Number) | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (50) |
| Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
| Place of publication: | Frankfurt [am Main] |
| Document Type: | Working Paper |
| Language: | English |
| Date of Publication (online): | 23.10.2012 |
| Date of first Publication: | 23.10.2012 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Licence (German): |  Veröffentlichungsvertrag für Publikationen ohne Print on Demand |
