[logic-ml] Prof. Olivier Danvy Lecture at NII Logic Seminar

[Makoto Tatsuta]

	 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