ALGI 07

************************************************************* * 第七回 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. なお，今年度は，冬にも東北で開催が企画されています．