POPL 2017 (series) / PEPM 2017 (series) / Workshop on Partial Evaluation and Program Manipulation /
Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk)
Any expression M in ULC (the untyped λ-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: environments, thunks, closures, etc. A compiled program is first-order functional and has a fixed set of working variables, whose number is independent of M. The generated LLL code in effect traverses the subexpressions of M.
We apply the techniques of game semantics to the untyped λ-calculus, but take a more operational viewpoint that uses less mathematical machinery than traditional presentations of game semantics. Further, the untyped lambda calculus ULC is compiled into LLL by partially evaluating a traversal algorithm for ULC.
Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | KeynotePEPM 2017 at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh Schultz University of Southern Denmark | ||
09:00 60mTalk | Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk) PEPM 2017 DOI | ||