Embedding the pi-calculus into a concurrent functional programming language

  • Correctness of program transformations and translations in concurrent programming is the focus of our research. In this case study the relation of the synchronous pi-calculus and a core language of Concurrent Haskell (CH) with asynchronous communication is investigated. We show that CH embraces the synchronous pi-calculus. The formal foundations are contextual semantics in both languages, where may- as well as should-convergence are observed. We succeed in defining and proving smart properties of a particular translation mapping the synchronous pi-calculus into CH. This implies that pi-processes are error-free if and only if their translation is an error-free CH-program Our result shows that the chosen semantics is not only powerful, but can also be applied in concrete and technically complex situations. The developed translation uses private names. We also automatically check potentially correct translations that use global names instead of private names. As a complexity parameter we use the number of MVars introduced by the transformation, where MVars are synchronized 1-place buffers. The automated refutation of incorrect translations leads to a classification of potentially correct translations, and to the conjecture that one global MVar is insufficient.

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 4.0]
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (60 [version 4.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:2020
Date of first Publication:2020/05/16
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2021/11/23
Tag:adequate translations; concurrency; functional programming; pi-calculus
Issue:[version 4.0] May 16, 2020
Page Number:54
First Page:1
Last Page:54
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