Output details
11 - Computer Science and Informatics
Imperial College London
A logical interpretation of the lambda-calculus into the pi-calculus, preserving spine reduction and types
<11> This paper presents a logical encoding of the lambda calculus into the pi calculus that is fundamentally different from all previous encodings, all more or less based on Milner's encoding. The logical encoding stands out because of its elegance and simplicity and has its foundation in the relation between sequent calculi and natural deduction, and allows for a better representation of beta-reduction. This approach has been picked up by others working in the area (Hirschkoff etal, CONCUR'12), and has led amongst others to a 'light' encoding of Parigot's lambda-mu in pi (van Bakel-Vigliotti, IFIPTCS'12). (Concur'09: 29% out 130)