第８回プログラミングおよびプログラミング言語ワークショップ(PPL2006)

プログラム

3/5/2006(日)
13:00-13:45 受付
13:45-14:00 オープニング
14:00-15:00 型解析　座長：Jacques Garrigue(名古屋大学)
  • Calculus of Constructionsのステージ化
    鈴木歩, 浅井健一(お茶の水女子大学)
  • Resource Usage Analysis for the Pi-Calculus
    末永幸平(東京大学), 小林直樹(東北大学), Lucian Wischik(Microsoft)
    出典：Seventh International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2006)
15:05-16:05 レビュー・チュートリアル　座長：石崎一明(日本アイ・ビー・エム)
  • フォーマルメソッドは夢か道具か？
    中島震(国立情報学研究所) [スライド]
16:20-17:40 ＸＭＬ　座長：千葉滋(東京工業大学)
  • XMLデータベースにおけるスキーマ更新操作の能力とスキーマ表現能力保存に関する完全性との関係
    橋本健二, 石原靖哲, 藤原融(大阪大学大学院情報科学研究科)
  • XML Information Set の C言語向け実装
    西岡真吾(国立情報学研究所)
  • XML Transformation Language Based On Monadic Second Order Logic
    稲葉一浩, 細谷晴夫(東京大学大学院情報理工学系研究科)
18:30-20:00 食事
20:00-22:00 ショートプレゼンテーション　座長：石崎一明(日本アイ・ビー・エム), 結縁祥治(名古屋大学/JST)
  • k-Pebble Tree Transducerに対する静的型検査の実効率
矢代武嗣(東京大学理学部情報科学科)
  • Tools and Experiments for Formal Verification of Operating Systems
Nicolas Marti(a), Reynald Affeldt(b), Akinori Yonezawa(a,b)
(a)Tokyo University, (b)AIST-RCIS
  • モデル検査のためのLinuxデバイスドライバのモデル化
樋口裕太, 結縁祥治, 阿草清滋(名古屋大学)
  • 文脈正規表現パターン
横山哲郎, 胡振江, 武市正人(東京大学)
  • α変換を考慮したβ変換の正当性の証明
山元かおり, 浅井健一(お茶の水女子大学)
  • シャッフル表現を扱うXML型検査
須田忠寛, 細谷晴夫(東京大学情報理工)
  • XMLの為の双方向変換言語
川中真耶, 細谷晴夫(東京大学)
  • スタックと双方向リストによる再帰的XML木変換の高速化
中野圭介(東京大学大学院情報理工学系研究科)
  • Calculus of Constructions を用いたインタプリタの作成
鈴木歩, 浅井健一(お茶の水女子大学)
  • MinCamlコンパイラにおける関数展開と特化
阪上紗里, 浅井健一(お茶の水女子大学)
  • 継続ジョインポイント
遠藤 侑介(a), 増原 英彦(b), 米澤 明憲(a)
(a)東京大学大学院情報理工学系研究科コンピュータ科学専攻, (b)東京大学大学院総合文化研究科広域システム科学系
  • 動的階層化モナドの設計と実装
米澤拓央(筑波大学)
  • マルチメディアコンテンツの静的解析へ向けて
斉藤新, 立石孝彰(日本IBM東京基礎研究所)
3/6/2006(月)
7:30-9:00 朝食
9:00-10:00 項書き換え　座長：酒井正彦(名古屋大学)
  • RAPT: A Program Transformation System based on Term Rewriting
    Yuki Chiba, Takahito Aoto, and Yoshihito Toyama(Research Institute of Electrical Communication, Tohoku University)
  • 書き換え帰納法における向き付け不能な等式の証明
    青戸等人(東北大学電気通信研究所)
10:05-11:05 関数型言語　座長：岡野浩三(大阪大学)
  • Private row types: abstracting the unnamed
    Jacques Garrigue(名古屋大学多元数理科学研究科)
  • Recursive modules for programming
    中田景子(京都大学), Jacques Garrigue(名古屋大学)
11:15-12:15 言語実装　座長：前田敦司(筑波大学)
  • Role-Based Refactoring of Crosscutting Concerns
    Jan Hannemann(University of Tokyo), Gail Murphy, Gregor Kiczales(University of British Columbia)
    出典：4th International Conference on Aspect-Oriented Software Development (AOSD 05)
  • 階層グラフ書き換え言語LMNtal 処理系とその応用例
    乾敦行, 原耕司, 水野謙, 上田和紀(早稲田大学大学院理工学研究科情報・ネットワーク専攻)
12:15-13:15 昼食
13:15-14:15 プログラム解析と変換(1)　座長：高橋孝一(産業技術総合研究所)
  • 様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明
    四熊尚方, 五十嵐淳(京都大学大学院情報学研究科知能情報学専攻)
  • Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives
    末永幸平(東京大学), 小林直樹(東北大学), 米澤明憲(東京大学)
    出典：International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2005)
14:20-15:20 レビュー・チュートリアル　座長：湯淺太一(京都大学)
  • COINSコンパイラ・インフラストラクチャの概要[スライド]
    中田育男(法政大学)
15:35-16:55 最適化　座長：千葉雄司(日立製作所)
  • Improving Sequenceを第一級の対象とするSchemeコンパイラ
    高野保真(電気通信大学大学院情報工学専攻), 岩崎英哉(電気通信大学情報工学k科)
  • 非再試行型レジスタ割付けとそのスピル最適化手法
    片岡正樹, 小川健一(早稲田大学大学院理工学研究科), 古関聰, 小松秀昭(日本IBM東京基礎研究所)、深澤良彰(早稲田大学大学院理工学研究科)
  • 実行時情報を利用した部分冗長除去とSSA形式への適用
    伊藤陽, 佐々政孝(東京工業大学情報理工学研究科数理・計算科学専攻)
17:00-18:20 ショートプレゼンテーション　座長：石崎一明(日本アイ・ビー・エム), 結縁祥治(名古屋大学/JST)
  • 抽象化によるグラフ書換系活性性質検証の一手法
Carl Frederiksen(a), 田辺良則(b,a)，萩谷昌己(a,c)
(a)東京大学大学院情報理工学系研究科, (b)産業技術総合研究所システム検証研究センター, (c)NTT コミュニケーション科学基礎研究所
  • 時間付きグラフ書換系の抽象化について
田辺良則(a,b)，萩谷昌己(b,c)
(a)産業技術総合研究所システム検証研究センター, (b)東京大学大学院情報理工学系研究科, (c)NTT コミュニケーション科学基礎研究所
  • 木上の双方向変換を利用したファイルマネージャの実現
松田一孝, 胡振江, 武市正人(東京大学大学院情報理工学系研究科)
  • FLWR Arraging: XQueryの冗長なエレメント構築子などの削除による書き換え
加藤弘之, 日高宗一郎(国立情報学研究所), 吉川正俊(名古屋大学)
  • XQueryへの垂直方向の再帰を含む融合変換の適用
日高 宗一郎, 加藤 弘之(国立情報学研究所), 吉川 正俊(名古屋大学)
  • 例外機構を持つ関数型言語のための計算資源使用法検証器
岩間太(東北大学情報科学研究科)
  • 実行履歴に基づくアクセス制御付き再帰プログラムのモデル検査
王静, 高田喜朗, 関 浩之(奈良先端科学技術大学院大学情報科学研究科)
  • Strutsアプリケーションのビジネスロジックのモデル検査支援方法の提案と例題実験
浜口優, 藤原貴之, 岡野浩三, 楠本真二(大阪大学情報科学研究科コンピュータサイエンス専攻)
  • 類似プログラムの提示ツール：Selene
渡邉卓也, 増原英彦(東京大学大学院総合文化研究科)
  • 助っ人：構成的な並列スケルトンによる並列プログラミングライブラリ
江本健斗(東京大学大学院情報理工学系研究科)
  • 書込バリアの追加が少ない複製に基づくコピーGC
鵜川始陽(a), 田中英行(b), 八杉昌宏(a), 湯淺太一(a)
(a)京都大学大学院情報学研究科, (b)京都大学工学部情報学科
  • Webアプリケーションのためのブラウザ内Scheme処理系
原悠(a), 鵜川始陽(b), 八杉昌宏(b), 湯淺太一(b)
(a)京都大学工学部情報学科, (b)京都大学大学院情報学研究科
  • Javaによる仮説に基づく整合性管理機構の実装
上野雄太, 岩見宗弘(島根大学総合理工学部数理・情報システム学科)
  • 双方向CTLによるJavaプログラム最適化器の生成
方玲, 佐々政孝(東京工業大学情報理工学研究科数理・計算科学専攻)
  • OCamlによるLMNtal実行時処理系 OCaMNtalの実装
工藤晋太郎, 乾敦行, 櫻井健, 上田和紀(早稲田大学大学院理工学研究科情報・ネットワーク専攻)
  • 非決定的LMNtalとその検証への応用
水野謙, 上田和紀(早稲田大学大学院理工学研究科情報・ネットワーク専攻)
  • Swapping Arguments and Results of Recursive Functions
森畑明昌, 筧一彦, 胡振江, 武市正人(東京大学)
  • Preplaned Dynamic Weaving
西澤無我(東京工業大学)
   
19:00-20:30 食事
20:30-22:00 デモ・ポスター発表　座長：石崎一明(日本アイ・ビー・エム), 結縁祥治(名古屋大学/JST)
3/7/2006(火)
7:30-9:00 朝食
9:00-10:00 λμ計算　座長：磯部祥尚(産業技術総合研究所)
  • 選言を含む自然演繹古典論理の強正規化性
    中澤巧爾(京都大学大学院情報学研究科), 龍田真(国立情報学研究所)
  • Relational parametricity and control
    Masahito Hasegawa(RIMS, Kyoto University/PRESTO, JST)
    出典：20th Annual IEEE Symposium on Logic in Computer Science (LICS2005)
10:05-11:05 レビュー・チュートリアル　座長：結縁祥治(名古屋大学/JST)
  • よく効く！ツリーオートマトン[スライド]
    大崎人士(産業技術総合研究所システム検証研究センター)
11:20-12:20 プログラム解析と変換(2)　座長：南出靖彦(筑波大学)
  • Improving Transition Predicate Abstraction for Verification Liveness Properties
    フレデリクセン、カール クリスチャン(東京大学)
  • An Algebraic Approach to Shortcut Fusion of Functions with an Accumulating Parameter
    勝股審也(数理解析研究所)
12:20-12:50 クロージング

戻る