コンピュータサイエンス研究会(2010年12月3日（金）)

2010.12.14

研究会名：コンピュータサイエンス研究会
開催日：2010年12月14日（火）15:00～17:00
題目： “Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)”
講師：Olivier Danvy氏　(Department of Computer Science, Aarhus University, Denmark)
開催場所：青葉山キャンパス情報科学研究科棟 2階大講義室

コンピュータサイエンス研究会　講演会の御案内

コンピュータサイエンス研究会
主査篠原　歩

下記のようにコンピュータサイエンス研究会の講演会を開催いたしますので，ご案内申し上げます．

日時：2010年12月14日（火）15:00～17:00
場所：青葉山キャンパス情報科学研究科棟2階大講義室（前回までと異なりますのでご注意ください）
題目：“Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)”
講師：Olivier Danvy（Department of Computer Science, Aarhus University, Denmark）
概要：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.
講師略歴：Olivier Danvy is interested in all aspects of programming languages, including programming. His other mother is the Universite Pierre et Marie Curie (aka. Paris VI: PhD, 1986; and Habilitation, 1993) and his other mother in law is Aarhus University (DSc, 2006), where he is currently supervising his 22nd PhD student, Ian Zerny.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.