ppl2009 jssst sig-ppl

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

プログラム

[home]
ロボット対策として,論文へのリンクにはbasicパスワード認証をかけてあります.(USER=ppl2009, PASS=ppl2009

注意: PPL2009 は国内の研究者に予備段階にある研究を発表する機会を与えるワークショップであるとともに,ここでの議論に基づき改良を加えた論文を国際会議や学術雑誌に投稿することを推奨しています.そのため,ここにあるオンライン予稿集は (ISBN,ISSNなどを持たない) 非公式のものであり,他の場所での出版を妨げるものではありません.
本ページ上のカテゴリ1論文は各著者によって提供されたものであり,著作権は各著者に属します.転載などに関しては各著作権者の許可を得る必要があります.
カテゴリ2は,査読付の国際会議または学術雑誌等で既発表(もしくは採録決定済)であるが国内で未発表の研究を紹介をする場であり,そこでの発表は論文の再出版・二重投稿などには該当しません.

NOTICE: PPL2009 aims to function as an informal workshop, which gives researchers an opportunity to disseminate their preliminary work and to get feedback from the Japanese research community. It also encourages submissions of revised papers to international conferences or to refereed journals. The online proceedings presented below are informal (neither ISBN nor ISSN is assigned) and should not preclude publication elsewhere.
Papers in the first category (C1) are provided by the contributing authors. Copyright of each document is maintained by the corresponding authors. The works may not be reposted or redistributed without the explicit permission of the copyright holder.
The second category (C2) is intended to help researchers disseminate their research to the domestic community by providing an opportunity to present papers that have already been accepted by international conferences or journals (but have not been presented in Japan before). Therefore, presentations in this category, which are informal, shouldn't be considered republication or the result of double submission.

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