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 <>
Submitted on : Wednesday, May 24, 2006 - 12:14:20 PM
Last modification on : Saturday, January 27, 2018 - 1:31:31 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