Pi-Lambda talk: Xinxin Liu
2007.09.13 |
| Date | Wed Sep 19 |
| Time | 11:15 — 12:00 |
| Location | DI-Turing-014 |
Title: A two value passing call-by-name CPS transformation
Date: Wednesday 19 September
Time 11:15-12:00
Location: Turing-014
Speaker:
Xinxin Liu
Laboratory of Computer Science
Institute of Software
Chinese Academy of Science
Abstract:
In this talk we present a CPS encoding for the call-by-name lambda
calculus.This encoding improves Plotkin's original encoding in that
basic constants and functional constants are encoded uniformly. The
trick to achieve this is to pass two values instead of one value in the
continuation. We will show that a relationship can be established
between terms and their encodings via call-by-name evaluation contexts,
and that the relationship can play an important role in proving both
simulation and translation theorems.
Biosketch:
Xinxin Liu
obtained his Phd degree from the University of Aalborg in
1992. He is now a research professor in the <a href =
"http://lcs.ios.ac.cn/lcs-eng/index.htm">Laboratory of Computer
Science in the Institute of Software at the Chinese Academy of
Sciences. His research interests include models of concurrency,
higher-order and concurrent programming, program specification and
verification.
Host:
Olivier Danvy