************************************************************* * 第七回 ALGI（代数，論理，幾何と情報科学研究集会）開催要項 * ************************************************************* 第六回に引き続き，第七回も JAMS 年会の分科会として，大阪大学コンベンショ ンホールにて（昨年と同じ場所です）以下で要領で開催します． 皆様の御参加をお待ちもうしあげております． 日時： 8月3日 13:00-16:40 8月4日 9:30-12:00 JAMS の年会は 8/2〜8/5 の日程ですが、その内上記時間帯 がALGIにわりあてられています。 会場： 大阪大学コンベンションセンター (大阪大学吹田キャンパス) プログラム： 【満員御礼】 空きのスロットがなくなりました． 8月3日 (13:00-16:40) 13:00-13:45 長谷川 真人 Girard translation and logical predicates 13:55-14:40 森 秀人 Chu Spaces and their Galois Connections 14:50-15:35 岡本 暁広 言語λεの拡張λεｌとこれらの強正規化可能性の証明 15:45-16:25 白旗 優 Title to be announced 夕方 懇親会 8月4日 (9:30-12:00) 9:30-10:15 竹内 泉 代数仕様の拡張について 10:25-11:10 樋口 証 Hypercategoryに基づく関数型言語の意味論 11:20-12:00 藤原 靖 認証プロトコルの動向紹介 講演梗概［講演者名五十音順］： ● 岡本 暁広(京大・情報学) 言語λεの拡張λεｌとこれらの強正規化可能性の証明 私は明示的環境を持つ型付きλ計算λεにメタレベルの代入を導入し た言語λεｌを考案した。言語λεｌの強正規化可能性を証明するこ とは、直接、言語λεの強正規化可能性の証明となる。本研究では、 さらに補助的な言語λεＮを定義し、λεｌの強正規化可能性をλε Ｎの弱正規化可能性に帰着させるという手法で証明を行なっている。 ● 白旗 優（慶應大・商学部） ● 竹内 泉（京大・情報学） 代数仕様の拡張について 代数仕様には必ず始代数があることが知られているが、既にある領域 に対して、代数仕様によって新たな領域を定義する場合には、必ずし も始代数があるとは限らない。この場合にも、何らかの意味で極小の 意味領域を作る方法を提案する。これは二階型付計算の上の論理によっ てなされる。 ● 長谷川真人（京大・数研） Girard translation and logical predicates We present a short proof of a folklore result: the "Girard translation" from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this talk is also intended as a tutorial on this proof technique for reasoning about relations between type theories. ● 樋口 証（北大・数学） Hypercategoryに基づく関数型言語の意味論 Resource consciousな関数型言語の意味論が、hypercategoryを使っ て自然に表現することができることを示し、また、それに基づいて設 計した言語を紹介する。hypercategoryはcategoryの自然な拡張であ り、図形を使って意味を表現ような種類の言語の意味を形式的に記述 するのに有用である。言語の意味は、プログラムに対して1つの hypercategoryを構成することによって与えられる。このようにして 作られた関数型言語は、例えばファイルアクセスのような手続きをも 関数として取り扱うことができる。 ● 藤原 靖（東芝） 認証プロトコル解析の動向紹介 ウェッブブラウザーやサーバで用いられるSSLなどの認証プロトコル は、セキュリティクリティカルシステムの重要な構成要素である。こ こでは認証プロトコル解析の形式的手法について、spi-計算をはじめ とする最近の動向を紹介する。 ● 森秀人（阪大・微研） Chu Spaces and their Galois Connections We consider the functor Sl from the category Chu of Chu spaces and Chu transformations to the category Slat of complete lattices and join preserving homomorphisms, which associates a Chu space C=(X,A,|=) to the complete lattice Sl(C) of the intersection closed family of subsets of X generated by the polar sets a^*:={x | x |= a } a in A. We show that Sl is *-autonomous functor with an injection Sl(C\multimap C') --> Slat(Sl(C),Sl(C')). Even when C\multimap C' is a trivial Chu space, the lattice Slat(Sl(C),Sl(C')) can be nontrivial, which suggests the study of the Slat-enriched category of Chu spaces with the hom-lattice Slat(Sl(C),Sl(C')) might be useful. 会場への交通： 地下鉄・北大阪急行線 千里中央駅(終点)から阪急バスで「阪大本部前」または 「茨城美穂ヶ丘」行 約10〜20分＊ 阪急電車京都線 茨木市駅から近鉄バスで「阪大本部前」行 約30分＊ JR東海道線 茨木駅から近鉄バスで「阪大本部前」行 約20分＊ いずれも「阪大本部前」下車 会場まで徒歩3分 以上は平成10年と同じですが，さらに，阪大医学部前まで大阪モノレールの 支線が開通した模様です． なお阪大案内図および阪大吹田キャンパス案内図を御覧ください． http://www.med.osaka-u.ac.jp/~derma/jsid/OUCC/OUCC.html なども役に立つかもしれません． 懇親会について： 何か考えます ... うーん，千里中央の屋上ビアガーデンというので如何でしょうか． 雨だったら...また別に考えることにして...... 宿の情報： コンベンションセンターのある阪大吹田キャンパスは千里にあります ので，千里中央あるいは北千里，南千里あたりの宿が一番近いと思い ます．江坂や大阪の中心地になると少し遠くなります． 千里の宿: 千里阪急ホテル (インターネット割引 (約10%) があります) 〒565 大阪府豊中市新千里東町2丁目1番D-1号 TEL06-872-2211 FAX06-832-2161 (地下鉄御堂筋線千里中央駅付近) 千里阪急ホテルは８／３は満室のようです。 オオサカ サンパレス シングル７０００円、電話０６ ６８７８ ３８０４ モノレールの万博公園駅前 （モノレールで阪大病院前まで行ける） ホテルマーレ南千里 〒565大阪府吹田市津雲台1-2-D9(阪急千里線南千里駅前) TEL:06-872-1911 FAX:06-872-0062 JR大阪駅、阪急梅田駅より阪急千里線にて約25分。 JR新大阪駅よりタクシーで15分。 江坂の宿一覧 大阪市近辺の宿一覧 幹事： 木下佳樹 P.S. なお，今年度は，冬にも東北で開催が企画されています．