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.

Download full text files

Export metadata

Author:Manfred Schmidt-SchaußORCiDGND, David SabelORCiDGND
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
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
Licence (German):License LogoDeutsches Urheberrecht