主催：NII 先端ソフトウェア工学国際研究センター（GRACEセンター）
http://grace-center.jp/
日時：2010年2月26日（金）10:00-12:00
場所：国立情報学研究所(NII) 20階会議室(2004) （地図）
参加費：無料
お問い合わせ：石川 冬樹 (f-ishikawa_AT_nii.ac.jp)_AT_を＠に書き換えてください。
参加をご希望の方は、セミナー前日までに下記よりご登録をお願いします。
http://grace-center.jp/regist/seminar
– – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – –
Details:
Title: Knuth’s 0-1-Principle and Beyond
First Speaker: Janis Voigtländer (University of Bonn)
Abstract:
We motivate a form of type-based reasoning by considering an old
meta-theorem about sorting by Knuth: a comparison-swap algorithm
sorts integers correctly if and only if it sorts Booleans correctly.
This theorem is very useful in analysing such algorithms and testing
their implementations. By rephrasing (and proving) Knuth’s statement
in terms of modern programming language concepts and techniques, one
obtains a general approach that can be applied to other classes of
algorithms as well. In particular, we present a corresponding result
for the task of parallel prefix computation.
Biography:
Janis Voigtländer is a junior professor at the University of Bonn.
His research interests are (functional) programming languages,
program transformation and verification, and formal approaches to
software construction. He is visiting NII on a JSPS Fellowship in February/March.
– – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – –
Title: Sound and Complete Validation of Graph Transformations
Second Speaker: Kazuhiro Inaba (National Institute of Informatics)
Abstract:
Transformation of graph structures is becoming more and more
important in many fields such as semi-structured database or
model-driven software development. There, graphs are often
associated with schemas that describe structural constraints on the graphs.
In this paper, we present a static validation algorithm based on
monadic second-order logic, for the core of a graph transformation
language UnCAL [Buneman et al., 2000].
Given a transformation and input/output schemas, our algorithm
statically verifies that any graph satisfying the input schema is
converted to a graph satisfying the output schema.
Our algorithm is sound, and moreover, complete in the sense that all
correct transformations are reported as correct with no false-
positive diagnostics. Furthermore, thanks to nice properties of the
structural recursion on which UnCAL is based on, the validation
remains decidable.
Biography:
Kazuhiro Inaba is a researcher at National Institute of Informatics.
His research interests include automata and formal language theory,
logic on graphs and trees, and XML transformation languages.
