From a Concurrent lambda-calculus to the pi-calculus
Roberto M. Amadio, Lone Leth, Bent Thomsen · 2008
. We explore the (dynamic) semantics of a simply typed - calculus enriched with parallel composition, dynamic channel generation, and input-output communication primitives. The calculus, called the k - calculus, can be regarded as the kernel of concurrent-functional languages such as LCS, CML and Facile, and it can be taken as a basis for the definition of abstract machines, the transformation of programs, and the development of modal specification languages. The main technical contribution of this paper is the proof of adequacy of a compact translation of the k -calculus into the ß-calculus. 1 Introduction Programming languages that combine functional and concurrent programming, such as LCS [4], CML [11] and Facile [5, 14], are starting to emerge and get applied -- some, like Facile, in industrial settings. These languages are conceived for programming of reactive systems and distributed systems. A main motivation for using such languages is that they offer integration of differe...