Colloquium Details
Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)
| Author: | Olivier Danvy Aarhus University, Denmark |
|---|---|
| Date: | October 21, 2010 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
| Host: | Zena Ariola |
Abstract
On the one hand, there are the De Morgan laws: it is clear how to repeatedly apply them to put a proposition in, say, negational normal form, with many small computational steps. On the other hand, such a normal form can be obtained with one big computational step by recursive descent.
On the one hand, there is the lambda-calculus: it is clear how to repeatedly apply its contraction rules to put a lambda-term in, say, weak-head normal form, if one exists, with many small computational steps. On the other hand, such a normal form can be obtained with one big computational step by recursive descent.
On the third hand, there are also abstract machines: state transition systems that will obligingly yields normal forms as well, if they exist.
There is no fourth hand in this talk: our goal is not to monkey with computation, but to demonstrate a profound structural unity in the various styles of semantic artifacts that have been proposed to specify computation: as a calculus with a reduction strategy, as a small-step system of proof rules, as a small-step system of reductions in contexts, as a small-step abstract machine, as a big-step abstract machine, as a continuation-passing big-step evaluation function, and as a direct-style big-step evaluation function. In the course of this talk, we will materialize this unity by using off-the-shelf program transformations to constructively inter-derive semantic artifacts for deterministic sequential programming languages, or, to be precise, their representation as functional programs.
Biography
Olivier Danvy is interested in all aspects of programming languages, including programming. He obtained his PhD and his Habilitation degrees in 1986 and 1993 from the Universite Pierre et Marie Curie (Paris VI) in France. He did not however let good enough alone and obtained a doctoral degree in 2006 from Aarhus University in Denmark, where he is currently supervising his 22nd PhD student. In his copious spare time, he co-edits the Springer journal Higher-Order and Symbolic Computation with Carolyn Talcott, and is serving as program chair for ICFP 2011. Since 1988, he is a Knight of the lambda-calculus and for what it is worth, a few years ago, he was measured to be the most acknowledged scientist in the CiteSeer data base.