Interpreting Functions as pi-calculus Processes: a Tutorial

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.