%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 3月9日(月) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 14:20--14:30 オープニング 14:30--16:00 セッション1 綾野貴之*, 堀泰祐**, 岩澤宏希*, 小川誠司*, 上田和紀*** *早稲田大学理工学部コンピュータ・ネットワーク工学科, **早稲田大学大学院基幹理工学研究科情報理工学専攻, ***早稲田大学理工学術院情報理工学科 統合開発環境によるLMNtalモデル検査 David NOWAK, 山田聖 産業技術総合研究所 情報セキュリティ研究センター Towards a Certified Implementation of a Cryptographically Secure Pseudorandom Bit Generator 末永幸平 東北大学 Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References (出典: 6th Asian Symposium on Programming Languages and Systems (APLAS 2008), LNCS 5356, pp. 155-170, 2008) 16:30--17:30 セッション2 (招待講演) 藤田善勝 リトルウイング リアルタイムゲームへの組み込みを目的としたScheme処理系の開発 17:30--18:30 セッション3 木村大輔*, 角谷良彦** *国立情報学研究所, **東京大学 古典S4様相論理に対応する計算系 勝股審也 京都大学数理解析研究所 A Characterisation of Lambda Definability with Sums via TT-Closure Operators (出典: 22nd International Workshop on Computer Science Logic (CSL 2008), LNCS 5213, pp. 278-292, 2008) 20:30--22:00 セッション4 (ポスター・デモ1) 湯淺太一 京都大学情報学研究科 SICP演習用に機能拡張したScheme-in-Java (デモ) 加藤祐輝*, 中澤巧爾** *京都大学工学部, **京都大学情報学研究科 存在型に対する型検査問題と型推論問題の同値性(ポスター) 西本匡志*, 川端英之**, 北村俊明** *広島市立大学情報科学部, **広島市立大学情報科学研究科 モバイルデバイスのためのビジュアルプログラミング環境の設計と実装(ポスター・デモ) 小笠原啓 有限会社ITプランニング マルチスレッド環境におけるGUIモデル(ポスター) 松本久志 東京工業大学理学部情報科学科 統合開発環境のためのプログラミング言語拡張フレームワーク(ポスター) 別役浩平 東京工業大学理学部情報科学科 ユーザ毎にカスタマイズ可能な Web アプリケーションの効率の良い実装方法(ポスター) ZAKIROV Salikh 東京工業大学大学院情報理工学研究科数理・計算科学専攻 スレッド別ゴミ集めによるキャッシュ効率向上(ポスター) 佐藤重幸 電気通信大学 GPU を利用する融合変換機構付きスケルトン並列フレームワーク(ポスター) アフェルト レナルド 産業技術総合研究所情報セキュリティ研究センター Coq上での組込み用途の冪剰余の検証(ポスター) 海野広志, 小林直樹 東北大学大学院情報科学研究科 Dependent Type Inference with Interpolants (ポスター) Jacques Garrigue 名古屋大学多元数理科学研究科 OCamlを型付ける？構造的多相性の健全性と型推論をCoqで(ポスター・デモ) 綾野貴之*, 堀泰祐**, 後町将人*, 岩澤宏希*, 小川誠司*, 上田和紀*** *早稲田大学理工学部コンピュータ・ネットワーク工学科, **早稲田大学基幹理工学研究科情報理工学専攻, ***早稲田大学理工学術院情報理工学科 LMNtalモデル検査の可視化環境(デモ) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 3月10日(火) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 9:00--10:00 セッション5 (招待講演) 吉田展子 Imperial College London Multiparty Asynchronous Session Types 10:30--11:30 セッション6 今井敬吾, 結縁祥治, 阿草清滋 名古屋大学 A full implementation of Session Types in Haskell 森畑明昌*, 胡振江**, 武市正人* *東京大学大学院情報理工学系研究科, **国立情報学研究所 動的計画法アルゴリズムを自己導出する結合子ライブラリ 13:00--13:30 セッション7 平石拓*, 八杉昌宏**, 馬谷誠二**, 湯淺太一** *京都大学学術情報メディアセンター, **京都大学情報学研究科 Backtracking-based Load Balancing (出典: 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP '09), 2009) 13:30--15:10 セッション8 (萌芽的研究) 蒲野茂幸, 佐々政孝 東京工業大学情報理工学研究科数理・計算科学専攻 SIMD最適化向けソースコードレベルでのコード変形 今橋孝典，佐々政孝 東京工業大学情報理工学研究科数理・計算科学専攻 種々の最適化の効果のモデル化と、それに基づく最適化列の効果の予測 山本雅洋, 大堀淳 東北大学電気通信研究所 変数の生存区間解析のためのSATソルバを用いた型推論アルゴリズム 酒井政裕, 今井健男 株式会社東芝 研究開発センター システム技術ラボラトリー CForge: C言語プログラムのための有界検査ツール Li Guoqiang*, 結縁祥治*, 足立正和** *名古屋大学 **豊田中央研究所 Environmental Simulation of Real-Time Systems with Nested Interrupts by Maude 15:30--17:00 セッション9 亀山幸義*, Oleg Kiselyov**, Chung-chieh Shan*** *筑波大学, **FNMOC, ***Rutgers University Shifting the Stage: Staging with Delimited Control (出典: ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation (PEPM'09), pp. 111-120, 2009) 木谷有沙, 浅井健一 お茶の水女子大学 限定継続を含む仮想機械導出のためのプログラム変換 増子萌，浅井健一 お茶の水女子大学 MinCaml コンパイラにおける shift/reset の実装 17:15-18:30 セッション10 (ショートプレゼンテーション) 橋本健二，石原靖哲，藤原融 大阪大学大学院情報科学研究科 XMLスキーマ進化におけるユーザ指定関係に基づく情報保存と更新操作群(ショート) 佐藤亮介，末永幸平，小林直樹 東北大学大学院情報科学研究科 木構造データに対するストリーム処理のための順序付き非線形型(ショート) 高田喜朗*, 森田剛正*, 関浩之** *高知工科大学, **奈良先端大学 情報流仕様に基づくアクセス権検査文自動挿入法(ショート) 丹生智也*，番原睦則**，田村直之** *神戸大学大学院工学研究科, **神戸大学学術情報基盤センター PrologからJavaへのトランスレータ処理系の設計と実装(ショート) 番原睦則*，丹生智也**，田村直之* *神戸大学学術情報基盤センター, **神戸大学大学院工学研究科 SAT変換に基づく制約ソルバーSugar (ショート) Phillip James*, 磯部祥尚**, Markus Roggenbach* *Swansea University, **産業技術総合研究所 Verifying Train Control Software - An exercise in SAT-based Model Checking (ショート) 磯部祥尚 産業技術総合研究所 定理証明器による双模倣等価性の自動証明(ショート、デモつき) 平井洋一 東京大学情報理工学系研究科コンピュータ科学専攻 トートロジーの中で代入極小でない中間論理の公理(ショート) Rossen MIKHOV 京都大学理学研究科数学・数理解析専攻数理解析系 Dual calculusのための、名前呼び、値呼び、および、必要呼び抽象機械(ショート) 道又淳一, 青戸等人, 外山芳人 東北大学電気通信研究所 多重Knuth-Bendix完備化における効率化手法の導入(ショート) 磯部耕己, 青戸等人, 外山芳人 東北大学電気通信研究所 S式書き換え系の停止性を保証するカリー化について(ショート) 村井正勝，青戸等人，外山芳人 東北大学電気通信研究所 基底項書換え系の合流性判定手続きの効率化(ショート) 20:30--22:00 セッション11 (ポスター・デモ2) 森口草介, 渡部卓雄 東京工業大学情報理工学研究科計算工学専攻 ジョインポイントモデルにおける操作の抽象化(ポスター) 江本健斗*, 胡振江**, 筧一彦***, 松崎公紀*, 武市正人* *東京大学情報理工学系研究科, **国立情報学研究所アーキテクチャ科学研究系, ***東京大学産学連携本部 プログラム運算に基づく最適化機能つき Fortress ライブラリ(ポスター・デモ) 櫻井加奈子, 浅井健一 お茶の水女子大学 証明木作成のためのGUI構築(ポスター・デモ) 上田やよい, 浅井健一 お茶の水女子大学 型付き対称λ計算における論理積型と論理和型の導入(ポスター) 対馬かなえ, 浅井健一 お茶の水女子大学 再帰と限定継続を扱うpolyvariantな部分評価に向けて(ポスター) 木津幸子 東京大学大学院情報理工学系研究科 Bi-HaXml: A Haskell Library for Bidirectional XML Transformations(ポスター・デモ) 松田一孝*, 胡振江**, 武市正人*, 穆信成*** *東京大学大学院情報理工学系研究科, **国立情報学研究所, ***Academia Sinica 木文法の構文解析を利用したプログラム逆計算 (ポスター) 橋本英樹*, 胡振江**, Julien Tesson***, 武市 正人* *東京大学, **国立情報学研究所, ***The University of Orleans プログラム運算のためのCoqライブラリ(ポスター・デモ) 八鍬豊, 上田和紀 早稲田大学大学院基幹理工学研究科情報理工学専攻 階層グラフ書換え言語LMNtalにおけるプロセスの等価性の提案と検討(ポスター) 塚田武志*, 五十嵐淳** *東北大学, **京都大学 Environment Classifiers の論理的基礎付け(ポスター) 廣瀬賢一*, 大谷順司*, 石井大輔**, 細部博史***, 上田和紀** *早稲田大学大学院基幹理工学研究科情報理工学専攻, **早稲田大学理工学術院情報理工学科, ***国立情報学研究所 制約概念に基づくハイブリッドシステムモデリング言語HydLaの実装(ポスター) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 3月11日(水) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 9:00--10:00 セッション12 当山学*, 増原英彦** *東京大学教養学部, **東京大学総合文化研究科 異なる型の値を返すアドバイスを許すアスペクト指向言語の織込機構 武山文信, 千葉滋 東京工業大学情報理工学研究科数理・計算科学専攻 アスペクトの相互作用を解消するアスペクトの提案 10:30--12:00 セッション13 浅田和之 京都大学数理解析研究所 Extensional Universal Types for Call-by-Value (出典: 6th Asian Symposium on Programming Languages and Systems (APLAS 2008), LNCS 5356, pp. 122-137, 2008) 立木秀樹*, 山田修司** *京都大学人間環境学研究科, **京都産業大学理学部 On Finite-time Computability Preserving Conversions (出典: 5th International Conference on Computability and Complexity in Analysis (CCA 2008), Electoric Notes in Theoretical Computer Science 221, pp. 299-308, 2008) 青戸等人 東北大学電気通信研究所 Sound Lemma Generation for Proving Inductive Validity of Equations (出典: 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), pp.13-24, 2008.) 12:00--13:00 クロージング %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%