Computing Publications

Publications Home » A Logical Interpretation of the L...

A Logical Interpretation of the Lambda-Calculus into the Pi-Calculus, Preserving Spine Reduction and Types

Steffen van Bakel, Maria Vigliotti

Conference or Workshop Paper
20th International Conference on Concurrency Theory (CONCUR'09)
0th International Conference on Concurrency Theory ( CONCUR'09)
Lecture Notes in Computer Science
Volume 5710
2009
Elsevier
Abstract

We define a new, output-based encoding of the lambda-calculus into the asynchronous pi-calculus – enriched with pairing – that has its origin in mathematical logic, and show that this encoding respects one-step spine-reduction up to substitution, and that normal substitution is respected up to similarity.

We will also show that it fully encodes lazy reduction of closed terms, in that term-substitution as well as each reduction step are modelled up to similarity.

We then define a notion of type assignment for the pi-calculus that uses the type constructor "arrow", and show that all Curry-assignable types are preserved by the encoding.

PDF of full publication (134 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.