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.
Type de document :
Rapport
RR-3470, INRIA. 1998
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00073220
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:14:20
Dernière modification le : jeudi 11 janvier 2018 - 16:43:48
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:38:43

Fichiers

Identifiants

  • HAL Id : inria-00073220, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

233

Téléchargements de fichiers

238