東北大学 電気通信研究所 外山研究室では、NUEセミナーを開催しています。 テーマはプログラム理論や定理自動証明を中心に、 情報科学の理論的なさまざまな話題をとりあげています。 興味をおもちの方はどなたでもフラリと気楽におたちより下さい。 NUEセミナーの開催は、 Logic メーリングリスト、 書き換えメーリングリスト、 "sonoteno"メーリングリストなどで、アナウンスが行われています。
| 日時 | 2005年9月30日 |
|---|---|
| 講演者 | 南出靖彦 (筑波大学) |
| 題目 | 定理証明系 Isabelle/HOL とその応用 |
| 要旨 | Isabelle/HOL は, 高階論理に基づく定理証明システムで, プログラム 言語,暗号プロトコルなど, 様々な対象の形式化, 検証に用いられている．本 講義では, Isabelle/HOL の基礎となる論理と使い方について紹介する. また， 応用例として，グラフの深さ優先探索の形式化，Isabelle/HOLを用いたCプログラムの検証について紹介する． |
| 日時 | 2005年9月16日 |
|---|---|
| 講演者 | Peter Dybjer (Chalmers University of Technology) |
| 題目 | Typed and untyped normalization by evaluation. |
| 要旨 |
Normalization by evaluation (nbe) is a new approach to
normalization algorithms and proofs. The idea is to interpret the
syntax in a suitable model and then extract the normal form from the
interpretation. It is essential that the model is constructive so that
the interpretation and extraction are computable functions. Normalization by evaluation has been developed for a variety of typed languages, and I shall show how such algorithms are suitable written in a language with dependent types such as Martin-Lof type theory. I shall then show how the method can be modified to deal with untyped languages. In particular I will show how an nbe-algorithm for untyped combinatory logic computes combinatory Bohm trees under lazy evaluation. |
| 日時 | 2005年4月15日 |
|---|---|
| 講演者 | Fer-Jan de Vries (University of Leicester) |
| 題目 | On the Construction and Properties of Normal Form Models of Lambda Calculus |
| 要旨 |
Confluent and normalising, infinite extensions of lambda
calculus can be made by adding infinite terms and infinite reduction
to finite lambda calculus and identification of certain meaningless
terms with $\bot$. Each such extension gives rise to a normal form
model of lambda calculus. We will show that there are many more such models than the three well-known models of respectively B\"ohm, Levy-Longo and Berarducci. Natural questions abound, like
|
| 日時 | 2005年3月24日 |
|---|---|
| 講演者 | 鈴木大郎 (会津大学) |
| 題目 | A Rewrite System with Incomplete Regular Expression Type for Transformation of XML Documents |
| 要旨 | We propose a new framework for transformations of XML documents based on an extension of regular expression type, called incomplete regular expression type. Incomplete regular expression type is a restricted second-order extension of regular expression (RE) type: An incomplete RE type can be applied to arbitrary RE types as its arguments. It is accomplished by introducing holes to types. We give a version of second-order rewrite systems, designed founded on our type system. Matching between a subterm with the left-hand side of rewrite rules yields a substitution that bind second-order terms to the variables of incomplete type. This feature is practically useful when we want to reuse ``the upper parts'' of XML documents in the transformation. We demonstrate that the introduction of incomplete regular expression type allows programmers much flexibility. After the presentation of formal definitions of our framework, we show some properties concerning for incomplete types. We also present a pattern match algorithm used in rewriting. |
| 日時 | 2005年2月9日 |
|---|---|
| 講演者 | Aart Middeldorp (University of Innsbruck) |
| 題目 | Tyrolean Termination Tool |
| 要旨 | In this talk I demonstrate the Tyrolean Termination Tool, a powerful and very fast tool for automatically proving termination of rewrite systems, both first-order and simply-typed applicative. The tool is based on the dependency pair method. Some of the underlying techniques will be explained in detail: subterm criterion and polynomial interpretations with negative coefficients. |
まで．