Embedding the pi-calculus into a concurrent functional programming language
- We investigate translations from the synchronous pi-calculus into a core language of Concurrent Haskell (CH). Synchronous messagepassing of the pi-calculus is encoded as sending messages and adding synchronization using Concurrent Haskell’s mutable shared-memory locations (MVars). Our correctness criterion for translations is invariance of may- and should-convergence. This embraces that all executions of a process are error-free if and only if this also holds for the translated program. We exhibit a particular correct translation that uses a fresh, private MVar per communication interaction and that is in addition adequate, and which is also fully abstract on closed expressions. A metaresult is that CH has the expressive power and the concurrency capabilities of the synchronous pi-calculus. We also automatically check variants of translations of synchronous communication into an asynchronous calculus where only an a priori fixed number of MVars per channel (and not per communication interaction!) is available. We obtain non-correctness results for classes of small translations, and exemplary argue for the correctness (and adequacy) for two translations with a higher number of MVars. We introduce a classification of the potentially correct translations.
Author: | Manfred Schmidt-SchaußORCiDGND, David SabelORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-633878 |
URL: | https://www2.ki.informatik.uni-frankfurt.de/papers/frank/frank-60v2.pdf |
Parent Title (German): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 60 [version 2.0] |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (60 [version 2.0]) |
Publisher: | Institut für Informatik, Fachbereich Mathematik und Informatik Goethe-Universität Frankfurt am Main |
Place of publication: | Frankfurt am Main |
Document Type: | Working Paper |
Language: | English |
Year of Completion: | 2019 |
Date of first Publication: | 2019/10/21 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2021/11/23 |
Tag: | adequate translation; concurrency; functional programming; pi-calculus |
Issue: | [version 2.0] October 21, 2019 |
Page Number: | 53 |
First Page: | 1 |
Last Page: | 53 |
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 |