HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Interpreting Functions as pi-calculus Processes: a Tutorial

Davide Sangiorgi 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper is concerned with the relationship between lambda-calculus and pi-calculus. The lambda-calculus talks about \emph{functions} and their\emph{applicative} behaviour. This contrasts with the pi-calculus, that talks aboutemph{processes} and their \emph{interactive} behaviour. Application is a special form of interaction, and therefore functions can be seen as a special form of processes. We study how the functions of the lambda-calculus (the \emph{computable} functions) can be represented as pi-calculus processes. The pi-calculus semantics of a language induces a notion of equality on the terms of that language. We therefore also analyse the equality among functions that is induced by their representation as pi-calculus processes. This paper is intended as a tutorial. It however contains some original contributions. The main ones are: the use of well-known \emph{Continuation Passing Style} transforms to derive the encodings into pi-calculus and prove their correctness; the encoding of \emph{typed} lambda-calculi.
Document type :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 12:14:20 PM
Last modification on : Friday, February 4, 2022 - 3:18:37 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:38:43 PM


  • HAL Id : inria-00073220, version 1



Davide Sangiorgi. Interpreting Functions as pi-calculus Processes: a Tutorial. RR-3470, INRIA. 1998. ⟨inria-00073220⟩



Record views


Files downloads