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.
Verfasserangaben: | 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 |
Titel des übergeordneten Werkes (Deutsch): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 60 [version 2.0] |
Schriftenreihe (Bandnummer): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (60 [version 2.0]) |
Verlag: | Institut für Informatik, Fachbereich Mathematik und Informatik Goethe-Universität Frankfurt am Main |
Verlagsort: | Frankfurt am Main |
Dokumentart: | Arbeitspapier |
Sprache: | Englisch |
Jahr der Fertigstellung: | 2019 |
Datum der Erstveröffentlichung: | 21.10.2019 |
Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Datum der Freischaltung: | 23.11.2021 |
Freies Schlagwort / Tag: | adequate translation; concurrency; functional programming; pi-calculus |
Ausgabe / Heft: | [version 2.0] October 21, 2019 |
Seitenzahl: | 53 |
Erste Seite: | 1 |
Letzte Seite: | 53 |
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 |