コンピュータサイエンス研究会　講演会

2012.01.13

研究会名：コンピュータサイエンス研究会

開催日：2012年1月13日（金）16:00～17:00

題目：“Reasoning About Multi-stage Programs”

講師：井上　純 (Department of Computer Science, Rice University)

開催場所：電子情報システム・応物系3号館206号室

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

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

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

日時：2012年1月13日（金）15:00～17:00
場所：電子情報システム・応物系3号館206号室
題目：“Reasoning About Multi-stage Programs”
講師：井上　純　（Department of Computer Science, Rice University）
要旨：
Multi-stage programming (MSP) is a style of writing program generators—programs which generate programs—supported by special annotations that direct construction, combination, and execution of object programs. Various authors have shown MSP to be effective in writing efficient programs without sacrificing genericity. However,correctness proofs of such programs have so far received limited attention, and approaches and challenges for that task have been largely unknown. In this thesis, I establish formal equational properties of the multi-stage lambda calculus and related proof techniques, as well as results that delineate the intricacies of multi-stage languages that one must be aware of.
In particular, I settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, can adding staging MSP to a language compromise the interchangeability of terms that held in the original language? Unfortunately it can, and more care is needed to reason about terms with free variables. Secondly, staging annotations, as the name “annotations” suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be the case? I give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy extensional facts, for example that functions agreeing on all arguments are equivalent? I develop a sound and complete notion of applicative bisimulation, which can establish not only extensionality but, in principle, any other valid program equivalence as well. These results improve our general understanding of staging and enable us to prove the correctness of complicated multi-stage programs.