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 conflicting 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.

Metadaten
Author:	Manfred Schmidt-Schauß ORCiD GND, David Sabel ORCiD GND
URN:	urn:nbn:de:hebis:30:3-270077
Parent Title (German):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 50
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):	2012/10/23
Date of first Publication:	2012/10/23
Publishing Institution:	Universitätsbibliothek Johann Christian Senckenberg
Release Date:	2012/10/29
Issue:	Version: 23 Oktober 2012
HeBIS-PPN:	344371085
Institutes:	Informatik und Mathematik / Informatik
Dewey Decimal Classification:	0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Sammlungen:	Universitätspublikationen
Licence (German):	Deutsches Urheberrecht

Open Access