[Prev][Next][Index][Thread]
paper on functions as pi-calculus processes
The paper below, a tutorial on the representation of functions as
pi-calculus processes, is availabile from
ftp://zenon.inria.fr/meije/theorie-par/davides/functionPItutorial.ps.gz
or from the WEB page
http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html#recent
It is thought as a draft of a chapter of a book that I am writing
with David Walker. Comments, remark, etc. are warmly appreciated!!
Davide Sangiorgi
***********
Title: Interpreting functions as pi-calculus processes: a tutorial
note: To appear as INRIA Technical Report RR-3470
pages: 92
Abstract: This paper is concerned with the relationship between
lambda-calculus and pi-calculus. The lambda-calculus talks about
functions and their applicative behaviour. This contrasts with the
pi-calculus, that talks about processes and their 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 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
Continuation Passing Style transforms to derive the encodings into
pi-calculus and prove their correctness; the encoding of typed
lambda-calculi.