Sumbitted
Abstract
Implicative Logic based encoding of the Lambda-calculus into the Pi-calculus.
by S. van Bakel and M.G. Vigliotti
Submitted
We study an output-based encoding of the Lambda-calculus with explicit substitution into the synchronous Pi-calculus -- enriched with pairing -- that has its origin in mathematical logic, and show that this encoding respects reduction.
We will define the notion of (explicit) spine reduction -which encompasses (explicit) lazy reduction- and show that the encoding fully encodes this reduction in that term-substitution as well as each single reduction step are modelled up to contextual similarity.
We show that all the main properties (soundness, completeness, and adequacy) hold for these four notions of reduction, as well as that termination is preserved.
We then define a notion of type assignment for the Pi-calculus that uses the type constructor arrow, and show that all Curry types assignable to Lambda-terms are preserved by the encoding.
