====================================================================== 第12回プログラミングおよびプログラミング言語ワークショップ PPL2010 確定版プログラム 発表時間: C1: 質疑応答も含め25分 C2: 質疑応答も含め20分 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 1日目 (3月3日) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 13:30 - 13:40 オープニング 13:40 - 15:10 (90分) セッション1 (C1) Towards Formal Construction of Assembly Arithmetic Functions from Pseudo-code Reynald Affeldt (AIST) (C1) 極性をもたないセッション型システム 今井 敬吾, 結縁 祥治, 阿草 清滋 (名古屋大学) (C2) Dependent Type Inference with Interpolants (出典: 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2009), pp. 277-288, 2009) Hiroshi Unno, Naoki Kobayashi (Tohoku University) (C2) Self Type Constructors (出典: 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA 2009), pp. 263-282, 2009) Chieri Saito, Atsushi Igarashi (Kyoto University) 15:10 - 15:30 休憩 15:30 - 16:30 セッション2 招待講演 オブジェクト指向言語余話 小野寺 民也 (日本IBM東京基礎研究所) 16:30 - 16:50 休憩 16:50 - 18:25 (95分) セッション3 (C1) 型付き対称λ計算と古典論理 上田 やよい, 浅井 健一 (お茶の水女子大学) (C1) 逐次一貫性下の知識伝達を表す直観主義様相論理 平井 洋一 (東京大学) (C1) 限定継続のための TDPE に向けて 対馬 かなえ, 浅井 健一 (お茶の水女子大学) (C2) Untyped Recursion Schemes and Infinite Intersection Types (出典: 13th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2010), to appear) Takeshi Tsukada, Naoki Kobayashi (Tohoku University) 18:25 - 20:30 夕食 20:30 - 22:00 セッション4 (ポスター・デモ1) (C3) ポスター 量的情報流の検証の困難性と可能性について 安岡 宏俊, 寺内 多智弘 (東北大学) (C3) ポスター 複数のプロンプトをもつ限定継続機構に対するCPS変換 高島 尚希, 亀山幸義 (筑波大学) (C3) ポスター マクロ木変換器の多項式時間逆実行 松田 一孝*, 中野 圭介**, 稲葉 一浩*** (*東京大学, **電気通信大学, ***国立情報学研究所) (C3) ポスター・デモ DrSchemeのWorldティーチパックを使ったゲームの作成 叢 悠悠*, 浅井 健一** (*お茶の水女子大学附属高等学校, **お茶の水女子大学) (C3) ポスター 論理関係によるスタック導入の正当性の証明 新井 祐美, 浅井 健一 (お茶の水女子大学) (C3) ポスター 分散動的アスペクト指向言語のアラウンドアドバイスの実装方法 早船 総一郎 (東京工業大学) (C3) ポスター 特定の観点上で連続するジョインポイントを選択可能なアスペクト指向言語 伊尾木将之 (東京工業大学) (C3) ポスター 関数型言語におけるべイズデバッグ 津田 均, 脇田 建 (東京工業大学) (C3) ポスター 排他制御機構に依らないクリティカルセクションの設計と実装に向けて 山田 佑二 (電気通信大学) (C3) ポスター Webアプリケーションにおけるサーバ・クライアント処理の分割支援 石橋 崇, 小宮 常康, 佐藤 喬, 多田 好克 (電気通信大学) (C3) ポスター・デモ LMNtal 階層グラフ可視化ツールUNYO-UNYO 斉藤 和佳子, 上田 和紀 (早稲田大学) (C3) ポスター Sound and Complete Validation of Graph Transformations 稲葉 一浩*, 日高 宗一郎*, 胡 振江*, 加藤 弘之*, 中野 圭介** (*国立情報学研究所, **電気通信大学) (C3) ポスター システム開発実務への証明支援器Coqの適用 今井 宜洋 (有限会社 ITプランニング) (C3) ポスター LLVMによるスクリプティング言語の高速化 小宮山 直貴, 倉光 君郎 (横浜国立大学) (C3) ポスター・デモ 例外処理を持つ関数型プログラムの停止性証明法 馬場 正貴, 酒井 正彦，濱口 毅，西田 直樹，坂部 俊樹，草刈 圭一朗 (名古屋大学) (C3) ポスター 広域分散環境で動作するSafeアンビエント処理系 宮本 琢也, 馬谷 誠二, 八杉 昌宏, 湯淺 太一 (京都大学) (C3) ポスター 安全で高速な共通計算基盤のための低水準の型付中間言語の検討 八杉 昌宏 (京都大学) (C3) ポスター・デモ プログラムの形式意味論演習システム 五十嵐 淳 (京都大学) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 2日目 (3月4日) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 9:00 - 10:00 セッション5 招待講演 Type-Based Reasoning for Real Languages Janis Voigtlander (University of Bonn) 10:00 - 10:25 休憩 10:25 - 12:00 (95分) セッション6 (C1) 最適値の並列探索のための Improving Value の Fortress 実装 江本 健斗*, 寺田 洋介*, 松崎 公紀**, 胡 振江**, 武市 正人* (*東京大学, **高知工科大学, ***国立情報学研究所) (C1) リダクションループに対する行列積に基づく自動並列化器の設計と実装 佐藤 重幸 (電気通信大学) (C1) shift/reset による Caml Light の拡張に向けて 増子 萌, 浅井 健一 (お茶の水女子大学) (C2) Extending AspectJ for Separating Regions (出典: 8th International Conference on Generative Programming and Component Engineering (GPCE 2009), pp. 45-54, 2009) Shumpei Akai, Shigeru Chiba (Tokyo Institute of Technology) 12:00 - 13:30 昼食 13:30 - 15:05 (95分) セッション7 (C1) Applied Pi-Calculusの計算論的健全性のパーズを用いない証明 ウベール・コモン-ルンド*, 萩谷 昌己**, 川本 裕輔***, 櫻田 英樹**** (*ENS Cachan, **東京大学, ***東京大学, 日本学術振興会特別研究員, ****NTTコミュニケーション科学基礎研究所) (C1) 条件式の解析によるSQLインジェクション脆弱性検査法の精度改善 西田 誠幸, 大橋 知典, Heng Li (拓殖大学) (C1) 情報流仕様に基づくアクセス権検査文自動挿入法 高田 喜朗*, 森田 剛正*, 関 浩之** (*高知工科大学, **奈良先端科学技術大学院大学) (C2) Dismantling MIFARE Classic (出典: 13th European Symposium on Research in Computer Security (ESORICS 2008), Lecture Notes in Computer Science 5283, pp. 97-114, 2008) Flavio D. Garcia, Gerhard de Koning Gans, Ruben Muijrers, Peter van Rossum, Roel Verdult, Ronny Wichers Schreur, Bart Jacobs (Radboud University Nijmegen) 15:05 - 15:25 休憩 15:25 - 17:00 (95分) セッション8 (C1) 多相型言語の変数名補完を行うEmacsモードの開発 後藤 拓実, 篠埜 功 (芝浦工業大学) (C1) 汎用的に証明木のGUIを作成する『Mikiβ』の開発 櫻井 加奈子, 浅井健一 (お茶の水女子大学) (C1) プログラム変換によるインタプリタからのコンパイラの導出 木谷 有沙, 浅井 健一 (お茶の水女子大学) (C2) Tool Support for Crosscutting Concerns of API Documentation (出典: 9th ACM International Conference on Aspect-Oriented Software Development (AOSD 2010), to appear) Michihiro Horie, Shigeru Chiba (Tokyo Institute of Technology) 17:00 - 17:20 休憩 17:20 - 18:30 セッション9 (ショート) (C3) ショート・デモ モデル検査ツールの拡張によるネットワークソフトウェアの検証 レオンワタナキット ワチャリン (東京大学) (C3) ショート さまざまな抽象データ構造をプリミティブとして扱うための プログラミング言語の設計 江木 聡志 (東京大学) (C3) ショート 木変換の逆正規性保存 稲葉 一浩 (国立情報学研究所) (C3) ショート 古典シークエント計算の強正規化可能性の構文論的証明 山口 洋平，中澤 巧爾 (京都大学) (C3) ショート バックトラックに基づく負荷分散の広域分散環境における評価 河野 卓矢, 八杉 昌宏, 平石 拓, 馬谷 誠二, 湯淺 太一 (京都大学) (C3) ショート 局所性を改善する世代別ごみ集めのSchemeインタプリタにおける実装と評価 渡邉 真人, 八杉 昌宏, 馬谷 誠二, 湯淺 太一 (京都大学) (C3) ショート Android DalvikVMにおける正確なごみ集め 松田 友希, 馬谷 誠二, 八杉 昌宏, 湯淺 太一 (京都大学) (C3) ショート 変性に基づく部分型のための半決定手続き 廣瀬 喜規, 五十嵐 淳 (京都大学) (C3) ショート L-closureを用いた真に末尾再帰的なSchemeインタプリタの実装 小島 啓史*, 八杉 昌宏*, 小宮 常康**, 平石 拓*, 馬谷 誠二*, 湯淺 太一* (*京都大学, **電気通信大学) 18:30 - 20:30 夕食 20:30 - 22:00 セッション10 (ポスター・デモ2) (C3) デモ 高階モデル検査のための述語抽象化とCEGAR 佐藤 亮介, 海野 広志, 小林 直樹 (東北大学) (C3) ポスター・デモ Dependent Types from Counterexamples 寺内 多智弘 (東北大学) (C3) ポスター 表現力の高いアドバイスを安全に記述できるアスペクト指向言語StrongRelaxAJ 当山 学, 青谷 知幸, 増原 英彦 (東京大学) (C3) ポスター・デモ 簡約過程の一般的可視化システムの実装 石川 ちひろ, 浅井 健一 (お茶の水女子大学) (C3) ポスター MetaOCamlを使った部分評価器の実装 岩井 亜里紗, 浅井 健一 (お茶の水女子大学) (C3) ポスター 暗黙的に型付けされる構造体のJava言語への導入 大久保 貴司 (東京工業大学) (C3) ポスター 関心事ごとに視点を切り替えてプログラムを編集できる統合開発環境の提案と実装 金澤 圭 (東京工業大学) (C3) ポスター 一級継続に基づくWebアプリケーションの動的更新 新井 一郎 (東京工業大学) (C3) ポスター 非S式言語における構文マクロの実現に向けて 荒井 浩，脇田 建 (東京工業大学) (C3) ポスター JavaScriptアプリケーションのLive Edit開発環境 吉永 卓矢, 脇田 建 (東京工業大学) (C3) ポスター 機器組込みシステムのための複製に基づくインクリメンタルコンパクション 鵜川 始陽*, 湯淺 太一** (*電気通信大学, **京都大学) (C3) ポスター ハイブリッドシステムモデリング言語HydLaの統合処理系 高田 賢士郎*, 廣瀬 賢一*, 大谷 順司*, 石井 大輔*, 細部 博史**, 上田 和紀* (*早稲田大学, **国立情報学研究所) (C3) ポスター・デモ 多相型言語の変数名補完を行うEmacsモードの開発 後藤 拓実, 篠埜 功 (芝浦工業大学) (C3) ポスター・デモ GRoundTram: 構造的再帰関数に基づく双方向グラフ変換システム 日高 宗一郎*, 胡 振江*, 稲葉 一浩*, 加藤 弘之*, 松田 一孝**, 中野 圭介*** (*国立情報学研究所, **東京大学, ***電気通信大学) (C3) ポスター 疑似乱数生成器の実装に対する暗号論的安全性の検証 山田 聖, David NOWAK (産業技術総合研究所) (C3) ポスター・デモ プロセス代数に基づく並行システムの動作解析のための逐次化ツール 磯部 祥尚 (産業技術総合研究所) (C3) ポスター スクリプティング言語KonohaによるLinuxカーネルデバイススクリプティング 井出 真広, 倉光 君郎 (横浜国立大学) (C3) ポスター・デモ アンビエント計算に基づくWebアプリケーション開発環境 外山 真, 馬谷 誠二, 八杉 昌宏, 湯淺 太一 (京都大学) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 3日目 (3月5日) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 9:00 - 10:30 (90分) セッション11 (C1) 累積変数をもつ木変換プログラムの並列木縮約に基づく並列計算 森畑 明昌 (東京大学, 日本学術振興会特別研究員) (C1) セマンティックマッピングによるキャスト操作の拡張 倉光 君郎 (横浜国立大学, JST/CREST) (C2) Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification (出典: 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pp. 495-508, 2010) Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno (Tohoku University) (C2) Polymorphic Fractional Capabilities (出典: 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science 5673, pp. 36-51, 2009) Hirotoshi Yasuoka, Tachio Terauchi (Tohoku University) 10:30 - 10:45 休憩 10:45 - 12:15 (90分) セッション12 (C1) 無限項書き換えシステムにおける強頭部正規化可能性の反証手続き 岩見 宗弘*, 青戸 等人** (*島根大学, **東北大学) (C1) 拡大手法に基づく項書き換え系の合流性自動証明 道又 淳一, 青戸 等人, 外山 芳人 (東北大学) (C2) Small-step and Big-step Semantics for Call-by-need (出典: Journal of Functional Programming, Vol. 19, No. 6, pp. 699-722, 2009) Keiko Nakata*, Masahito Hasegawa** (*Tallinn University of Technology, **Kyoto University) (C2) Trace-Based Coinductive Operational Semantics for While: Big-step and Small-step, Relational and Functional Styles (出典: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Lecture Notes in Computer Science 5674, pp. 376--390, 2009) Keiko Nakata, Tarmo Uustalu (Tallinn University of Technology) 12:15 - 13:00 クロージング ======================================================================