日々の流転

λ. "Types for Verification"

ワークショップの"Types for Verification"一日目。5時起き。7時半羽田発8時半伊丹。園田駅で反対側の出口に出てしまったりもしたけれど、なんとか始まる前に着くことが出来た。それはそうと、関西ではスイカもパスネットもバスカードも使えないのか……なんかほんと遠くにきたって感じだ。

λ. Per Martin-Löf (Stockholm University, on sabbatical at Sato-Lab, Kyoto U.) "100 years of Zermelo's axiom of choice: what was the problem with it?"

An analysis of Zermelo's axiom of choice in constructive type theory reveals that the problem with it is not the existence of the choice function but the extensionality of it, which is not visible in an extensional framework where all functions are by definition extensional.

"Intuitionistic Type Theory"にも選択公理の話は少しは出ていたはずなのだけど、すっかり忘れている私。まずいなー。(追記予定)

後で聞いた話によると、この話は3月に三田で話した内容とほぼ同じだとか(Proof Theory and its Applicationsに関する合同セミナーかな)。

【追記】 http://comjnl.oxfordjournals.org/cgi/reprint/49/3/345も参照。というか、後で読む。

λ. Masahiko Sato (佐藤 雅彦) (Kyoto University) "A simple theory of expressions"

We propose a framework called Natural Framework, which is used to present mathematics in a formal and convenient way. We are particularly interested in formalizing not only ordinary mathematics but also metamathematics. In this talk, we present a simple theory of expressions which we use as the underlying framework for Natural Framework.

例のCALの内部で使った表現なのかな。どの辺りがうれしいのかいまいちよく分からなかった。(追記予定)

λ. Peter Dybjer (Chalmers University of Technology, visiting AIST CVS) "Martin-LöF type theory and the logic of functional programs"

Martin-Löf type theory is a foundational framework for constructive mathematics and computer programming which is based on the Curry-Howard interpretation of propositions as types. This interpretation can be extended to an interpretation of Heyting arithmetic can in Martin-Löf type theory. In the opposite direction we have the interpretation of Martin-Löf type theory in a first-order theory of combinators given by Aczel 1974. This interpretation is closely related to the informal meaning explanations underlying Martin-Löf type theory.

In this talk I will review Aczel's interpretation and discuss its relevance for the CoVer project (Combining Verification Methods in Software Developement). The goal of this project is to build a tool where functional programs can be verified by a combination of testing and interactive and automatic theorem proving. The functional programs are written in Haskell and thus the underlying logic need to contain inference rules for reasoning about general recursive and lazy programs, and I will discuss some possible approaches.

Coverプロジェクトの一部であるAgda/Alfaで用いるロジックの話。(追記予定)

λ. John Hughes (Chalmers University of Technology, visiting AIST CVS) "Random Testing with QuickCheck"

One important use of formal specifications is in software testing: specifications can be used both as test oracles, and also for test case selection. The latter may require manual analysis of the specification, though, making this step relatively costly and indirect.

In this talk I will describe a tool we have developed, which provides a restricted (but surprisingly powerful) formal specification language in which specifications can be interpreted directly as test suites. The key idea is to interpret universal quantification in properties as random test case generation. The tool works well in practice, and the ideas have been used to test functional, imperative, and concurrent code. The original implementation is now distributed along with the standard Haskell compilers, and the ideas have been ported to (at least) ML, Scheme, Erlang, Python, and Mercury.

QuickCheckの紹介。 QuickCheckのアイディア自体は非常に単純。QuickCheckはテストのためのフレームワークなのだけど、個々のテストデータはユーザが記述するのではなく、システムがランダムに自動生成する。そして、ユーザによって記述された性質が、それらのランダムに生成されたテストデータに対して満たされているかをチェックする。もちろん、実際には色々な問題があるのだけど、それらはHaskellらしい方法で解決されてる。(追記予定)

Erlang, C. Scheme, Common Lisp, Python, Mercury, ML, ... に移植されているそうだ。Pythonに負けるのは癪なのでRubyにも移植しよう。

それはそうとプレゼンがとても上手だった。私もこんな発表が出来るようになりたいものだ。(追記予定)

λ. Yoshiki Kinoshita (AIST Research Center for Verification and Semantics) "Is modal mu calculus enough for verifying reactive systems?"

(追記予定)