----Next_Part(Fri_May__7_03_43_23_2004_219)--
Content-Type: Text/Plain; charset=iso-2022-jp
Content-Transfer-Encoding: 7bit

FYI.

5/11, 5/12 に、産総研尼崎サイトに型理論・Haskell方面の研究者(スウェー
デン・Chalmers大)の関係者が来るので、workshop を開くです。

いい機会なので、行って話を聴いてくるつもりです。

--
酒井 政裕 / Masahiro Sakai


--
ML: haskell-jp / quickml.com
使い方: http://QuickML.com/
----Next_Part(Fri_May__7_03_43_23_2004_219)--
Content-Type: Message/Rfc822
Content-Transfer-Encoding: 7bit

Return-Path: <clc-open-admin / m.aist.go.jp>
Received: from rpsmtp1.aist.go.jp by smtp1.aist.go.jp  with ESMTP id i3R6kBRW022404; Tue, 27 Apr 2004 15:46:11 +0900 (JST) env-from (clc-open-admin / m.aist.go.jp)
Received: from ml2.aist.go.jp by rpsmtp1.aist.go.jp  with ESMTP id i3R6k98V021834; Tue, 27 Apr 2004 15:46:09 +0900 (JST) env-from (clc-open-admin / m.aist.go.jp)
Received: from m.aist.go.jp by ml2.aist.go.jp with ESMTP id i3R6k843028555; Tue, 27 Apr 2004 15:46:08 +0900 (JST) env-from (clc-open-admin / m.aist.go.jp)
Received: from rpsmtp1.aist.go.jp by ml2.aist.go.jp with ESMTP id i3R6k343028526; Tue, 27 Apr 2004 15:46:03 +0900 (JST) env-from (takeyama / ashi.o.aist.go.jp)
Received: from ashi.o.aist.go.jp by rpsmtp1.aist.go.jp  with ESMTP id i3R6k2CS021797; Tue, 27 Apr 2004 15:46:02 +0900 (JST) env-from (takeyama / ashi.o.aist.go.jp)
Received: from ashi.o.aist.go.jp (localhost [127.0.0.1]) by ashi.o.aist.go.jp (8.12.10/8.12.10) with ESMTP id i3R6k2Ui004880; Tue, 27 Apr 2004 15:46:02 +0900
Received: (from takeyama@localhost) by ashi.o.aist.go.jp (8.12.10/8.12.10/Submit) id i3R6k2iZ004877; Tue, 27 Apr 2004 15:46:02 +0900
Date: Tue, 27 Apr 2004 15:46:02 +0900
From: takeyama <makoto.takeyama / aist.go.jp>
Reply-To: makoto.takeyama / aist.go.jp
Subject: [clc-open 00023] CFP: workshop "Types for Verification"
To: clc-open / m.aist.go.jp,
 logic-ml / logic.jaist.ac.jp,
 sonoteno / m.aist.go.jp
Cc: slacs-kanji / sato.kuis.kyoto-u.ac.jp,
 algi-ctl / m.aist.go.jp,
 rewriting-ctl / m.aist.go.jp,
 informatics / m.aist.go.jp
Message-Id: <200404270646.i3R6k2iZ004877 / ashi.o.aist.go.jp>
X-ML-Name: clc-open
X-Mail-Count: 00023
X-MLServer: fml [fml 4.0 STABLE (20030202/4.0.4_ALPHA)]; post only (only members can post)
X-ML-Info: If you have a question, send e-mail with the body "help" (without quotes) to the address clc-open-ctl / m.aist.go.jp; helpailto:clc-open-ctl / m.aist.go.jp?bodyセ
ユュチコ モナヘノッアョアエョウ ィユゥ ニフノヘッアョアエョウ ィモマュククオケュエソムソユソ ソノモマュククオケュエソムソ鴉ソチミナフッアーョウ ナッイアョイ ィウクカュュュゥ ヘユフナッオョー ィモチヒチヒノゥ
ヘュヨコ アョー ィ  モナヘノ アョアエョウ ュ 「ユ「ゥ
ミコ 
フュノコ ュョョョョ
フュモコ  ロ エョー モヤチツフナ ィイーーウーイーイッエョーョエ゜チフミネチゥン
フュミコ シコュタョョョセ
フュマコ シコュュタョョョセ
フュネコ シコュュタョョョソセ
フュユコ シコュュタョョョソセ
テュヤコ ッサ
 マュイーイイュハミ
テュヤュナコ キ

ワークショップ   "Types for Verification" のご案内
CFP: workshop "Types for Verification"

皆様、

(して受け取られた方、あいすみません)
産総研システム検証研究センター(AIST CVS)の武山とます。

数理的検証に関連する理論と実践に強い伝統を持つスェーデンから代な先
生方がお三方関西に(?)されるのを機会に、下記のようにワークショップ
"Types for Verification" を開催する運びとなりましたのでご案内い
たします。基盤的体系の考えかたから活用のための技泙派広く議論できえ
機会になればと考えますので、皆様ふるってのご参加をお待ち上げます。

参加自由ですが、センター施設への来訪者受け付けの関係上 参加ご希望の旨
武山 makoto.takeyama / aist.go.jp まで事前に御一報いただければ幸いです。

(また cc させて頂いた特定の連絡専用リストの幹事様等におかれましては、
御手数ですが、適当とされる場合は forward していただければ幸いです。)

Dear All,  (apologies for multiple copies)

This is a call for participation for the workshop "Types for Verification,"
held to coincide the chance gathering in Kansai of three representative
scholars from Sweden in areas related to the theory and practice of
systems verification.  We are looking foward to your participation in
free discussions ranging from foundational systems to technologies for
applications.

There is no fee or a limit on available seats, but please let me
(makoto.takeyama / aist.go.jp) know that you are coming, for registering
of site visitors.

Best Wishes,

Makoto Takeyama

Research Center for Verification and Semantics
National Institute of Advanced Industrial Science and Technology (AIST)
phone: 06-6494-8079
email: makoto.takeyama / aist.go.jp


            記

Workshop "Types for Verification"

Date : 2004 May 11 (Tue) kl. 09.50  ~  May 12

Venue: AIST Research Center for Verification and Semantics
       A-building, Conference Room 2
       (access guide
         http://unit.aist.go.jp/informatics/WEB/English/engindex.html)

       産業技
躪膰Φ システム検証研究センター A棟1F第2会議室
       (瀉蔵661-0974 兵庫県尼崎市若王寺3-11-46
               産業技
躪膰Φ慇哨札鵐拭柴崎サイエ
        アクセスガイド:  http://unit.aist.go.jp/informatics "アクセス" ページ)

*Program*

May 11 (Tue)

10.00 -- 10.50

   Per Martin-Loef (Stockholm University, on sabbatical at Sato-Lab, Kyoto U.)
              [oe -> \"o]
                   
   "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.

11.00 -- 11.50

   Masahiko Sato (Kyoto University)

   "A simple theory of expresions"

   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 uderlying
   framework for Natural Framework.

14.00 -- 14.50

   Peter Dybjer (Chalmers University of Technology, visiting AIST CVS)

   "Martin-Loef type theory and the logic of functional programs"

   Martin-Loef 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-Loef type theory. In the opposite direction
   we have the interpretation of Martin-Loef 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-Loef 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.

15.00 -- 15.50

   John Hughes (Chalmers University of Technology, visiting AIST CVS)

   "Random Testig 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.

   [上で誤解を招きがちにい討靴泙い泙靴燭;戴瘡紊諒です。]

16.00 -- 16.50

   Yoshiki Kinoshita (AIST Research Center for Verification and Semantics)

   "Is modal mu calculus enough for verifying reactive systems?"

(17.00 --

   Eating out )

May 12 (Wed)

9.00 -- 9.50

   Ken-etsu Fujita (Shimane University)

   TBA


contact: makoto.takeyama / aist.go.jp
         06-6494-8079

以上


----Next_Part(Fri_May__7_03_43_23_2004_219)----