Title
The geometry of optimal lambda reduction
Abstract
Lamping discovered an optimal graph-reduction implementation of the &lgr;-calculus. Simultaneously, Girard invented the geometry of interaction, a mathematical foundation for operational semantics. In this paper, we connect and explain the geometry of interaction and Lamping's graphs. The geometry of interaction provides a suitable semantic basis for explaining and improving Lamping's system. On the other hand, graphs similar to Lamping's provide a concrete representation of the geometry of interaction. Together, they offer a new understanding of computation, as well as ideas for efficient and correct implementations.
Year
DOI
Venue
1992
10.1145/143165.143172
POPL
Keywords
Field
DocType
suitable semantic basis,optimal graph-reduction implementation,concrete representation,new understanding,optimal lambda reduction,operational semantics,mathematical foundation,correct implementation,geometry of interaction
Graph,Operational semantics,Interaction nets,Programming language,Geometry of interaction,Computer science,Implementation,Theoretical computer science,Computation,Lambda
Conference
ISBN
Citations 
PageRank 
0-89791-453-8
118
8.90
References 
Authors
5
3
Search Limit
100118
Name
Order
Citations
PageRank
Georges Gonthier12275195.06
Martín Abadi2120741324.31
Jean-jacques Lévy393295.41