[kisoron-ml] Prof. Olivier Danvy Lecture at NII Logic Seminar
Makoto Tatsuta
tatsuta at nii.ac.jp
Thu Dec 9 00:30:05 JST 2010
Prof. Olivier Danvy Lecture at NII Logic Seminar
Date: December 16, 2010, 14:00--16:00
Place: National Institute of Informatics, Room 2005 (20th floor)
場所: 国立情報学研究所 20階 2005室
(半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
(地図 http://www.nii.ac.jp/introduce/access1-j.shtml)
Speaker: Prof. Olivier Danvy (University of Aarhus)
Title: Small-step and Big-step Aspects of Computation
(A Walk in the Semantic Park)
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 second 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.
問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta at nii.ac.jp
http://research.nii.ac.jp/~tatsuta
More information about the Kisoron-ml
mailing list