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
Verfasserangaben:	Manfred Schmidt-Schauß ORCiD GND, David Sabel ORCiD GND
URN:	urn:nbn:de:hebis:30:3-270077
Titel des übergeordneten Werkes (Deutsch):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 50
Schriftenreihe (Bandnummer):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (50)
Verlag:	Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Verlagsort:	Frankfurt [am Main]
Dokumentart:	Arbeitspapier
Sprache:	Englisch
Datum der Veröffentlichung (online):	23.10.2012
Datum der Erstveröffentlichung:	23.10.2012
Veröffentlichende Institution:	Universitätsbibliothek Johann Christian Senckenberg
Datum der Freischaltung:	29.10.2012
Ausgabe / Heft:	Version: 23 Oktober 2012
HeBIS-PPN:	344371085
Institute:	Informatik und Mathematik / Informatik
DDC-Klassifikation:	0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Sammlungen:	Universitätspublikationen
Lizenz (Deutsch):	Deutsches Urheberrecht

Open Access