jssst sig-ppl

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

1日目 (3月5日) 午後の部

13:20 - 13:30 オープニング
13:30 - 14:20 セッション1  型  (座長 : 海野 広志 (筑波大学))
顕在的契約計算における代数的データ型 [C1]
関山 太朗 (京都大学), 西田 雄気 (京都大学), 五十嵐 淳 (京都大学)
単純かつ実用的な静的サイズ検査つき線形代数演算ライブラリ [C1]
阿部 晃典 (東北大学), 住井 英二郎 (東北大学)
14:30 - 15:30 セッション2  招待講演 (1)  (座長 : 中田 秀基 (産業技術総合研究所))
Rubyの国際標準化と言語仕様記述
中田 育男 (筑波大学 名誉教授)
Rubyは2012年4月にISO規格として制定された。その経過と内容および今後の課題について報告する。規格として提案するための言語仕様書の作成は2008年にIPAに設置されたRuby標準化検討委員会で行った。その内容はRuby処理系の動作を抽象化したものである。Rubyではいろいろな書き方が許されているので、その文法記述は簡単ではない。複雑な構文規則や意味規則を記述するための工夫が必要である。その記述結果をチェックするために構文解析器も試作した。しかし、今回の規格はバージョン1.8を基にしており、その後のバージョンと異なる部分は記述を避けている。またライブラリもごく基本的なものだけを記述している不完全なものである。今後、より完全な規格を作成する必要がある。
15:40 - 16:50 セッション3  言語拡張  (座長 : 増原 英彦 (東京工業大学))
Composable User-Defined Operators That Can Express User-Defined Literals [C2]
Kazuhiro Ichikawa (The University of Tokyo), Shigeru Chiba (The University of Tokyo)
より柔軟な非同期実行記述を可能にするライブラリのための新しい限定継続演算子に向けて [C1]
山口 洋 (東京大学), 千葉 滋 (東京大学)
SML#のSQL統合機能への行集約機能の実装 [C1]
斎藤 皓 (東北大学), 上野 雄大 (東北大学), 森畑 明昌 (東北大学), 大堀 淳 (東北大学)
17:00 - 18:10 セッション4  並列・並行処理  (座長 : 前田 敦司 (筑波大学))
Do C and Java Programs Scale Differently on Hardware Transactional Memory? [C2]
Rei Odaira (IBM Research - Tokyo), Jose G. Castanos (IBM Research - T. J. Watson Research Center), Takuya Nakaike (IBM Research - Tokyo)
Dalvik VMにおける並行メモリ割当ての実現 [C1]
中野 陽基 (電気通信大学), 鵜川 始陽 (電気通信大学)
大規模ワークフロー用スケジューラ実装のためのライブラリ設計 [C1]
鈴木 康平 (三重大学), 松本 真樹 (三重大学), 大野 和彦 (三重大学)

1日目 (3月5日) 夜の部

20:00 - 22:00 セッション5  ポスター・デモ (1)  
辞書変換を用いたマルチプルインスタンスの設計と実装 [C3]
江島 将司 (熊本大学), 桂 直人 (熊本大学), 木山 真人 (熊本大学), 芦原 評 (熊本大学)
Agda による各種コンパイラ最適化プログラムの定式化 [C3]
門脇 香子 (お茶の水女子大学)
メモリレイアウトを切り替えられるグラフ解析プログラム向けJavaコンパイラ [C3]
汐田 徹也 (東京大学), 佐藤 芳樹 (東京大学), 千葉 滋 (東京大学)
BDDを用いた高階モデル検査アルゴリズム [C3]
寺尾 拓 (東京大学), 小林 直樹 (東京大学)
文脈に依存したグラフ書き換え系の設計と実装 [C3]
奈良 耕太 (早稲田大学), 上田 和紀 (早稲田大学)
一般化量化子を含む自然論理に対する依存型意味論の完全性 [C3]
中野 悠紀 (お茶の水女子大学), 戸次 大介 (お茶の水女子大学, 国立情報学研究所, 科学技術振興機構 CREST)
Generic GluonJ に向けて [C3]
小島 健介 (京都大学, JST CREST), 五十嵐 淳 (京都大学, JST CREST)
LMNtal実行時処理系SLIMにおけるグラフ構造探索の計算量改善 [C3]
青山 龍一 (早稲田大学), 上田 和紀 (早稲田大学)
有効にする破壊的クラス拡張を切り替えられるモジュール機構 Method Shells [C3]
竹下 若菜 (東京大学), 千葉 滋 (東京大学)
フィーチャ指向プログラミング言語: FeatureGluonJ [C3]
武山 文信 (東京大学)
スタックの高さの特徴付けによる言語が決定性文脈自由でないことの証明 [C3]
上里 友弥 (筑波大学), 南出 靖彦 (筑波大学)
動的に信用の変化するセキュリティプロトコルの自動検証のための型システム [C3]
川田 禎彬 (東京大学), 小林 直樹 (東京大学)
Applications of Redefining EDSL Expression Semantics at Load-Time [C3]
Maximilian Pascal Scherr (東京大学), Shigeru Chiba (東京大学)
PGASプログラムのためのプロファイリングツールの開発 [C3 (デモ)]
板橋 晟星 (東京大学), 佐藤 芳樹 (東京大学), 千葉 滋 (東京大学)
一階詳細化を用いた関数型プログラムの関係的性質の検証 [C3]
佐藤 亮介 (東京大学), 浅田 和之 (東京大学), 小林 直樹 (東京大学)
社会シミュレーションを並列化するための新しい言語機構の研究へ向けて [C3]
夏 澄彦 (東京大学), 佐藤 芳樹 (東京大学), 千葉 滋 (東京大学)
文脈指向言語JCopへの型検査器の構成と実装 [C3]
井上 裕昭 (京都大学), 五十嵐 淳 (京都大学)
型に基づく実行時契約検査機構の実装 [C3 (デモ)]
西田 雄気 (京都大学), 関山 太朗 (京都大学), 五十嵐 淳 (京都大学)
状態遷移機械を構成するための新しいFRPコンビネーターの提案 [C3]
小笠原 啓 (有限会社ITプランニング)
コンテナ型仮想環境における計算資源交換に基づく性能最適化 [C3]
中森 亮介 (筑波大学), 阿部 聖昂 (筑波大学), 前田 敦司 (筑波大学)
ワールドによるプログラミング [C3]
木下 修司 (奈良先端科学技術大学院大学), 木下 佳樹 (神奈川大学)
限定継続を備えた計算体系へのソフトウェア契約の導入 [C3 (デモ)]
上田 宗一郎 (京都大学), 関山 太朗 (京都大学), 五十嵐 淳 (京都大学)
フィードバック指向ランダムテストを用いたQuickCheckの改良 [C3]
矢藤 康祐 (東京大学), 坂本 一憲 (国立情報学研究所), 石川 冬樹 (国立情報学研究所), 本位田 真一 (東京大学, 国立情報学研究所)
CoqによるCプログラムの検証基盤のデモ [C3 (デモ)]
アフェルト・レナルド (産業技術総合研究所), 坂口 和彦 (筑波大学)

2日目 (3月6日) 午前の部

8:45 - 9:55 セッション6  自動検証  (座長 : 稲葉 一浩 (Google))
Automatic Termination Verification for Higher-Order Functional Programs [C2]
Takuya Kuwahara (University of Tokyo), Tachio Terauchi (Nagoya University), Hiroshi Unno (University of Tsukuba), Naoki Kobayashi (University of Tokyo)
高階木変換器の自動検証のための反例発見と抽象化改良 [C1]
松本 雄磨 (東京大学), 小林 直樹 (東京大学), 海野 広志 (筑波大学)
帰納的定理自動証明のための項書き換えシステム自動変換 [C1]
佐藤 洸一 (東北大学), 菊池 健太郎 (東北大学), 青戸 等人 (東北大学), 外山 芳人 (東北大学)
10:05 - 11:05 セッション7  招待講演 (2)  (座長 : 中野 圭介 (電気通信大学))
自動改札機ソフトウェアの品質向上の取組み
幡山 五郎 (オムロンソーシアルソリューションズ)
鉄道の自動改札機に搭載されているソフトウェアの信頼性を高めるために、開発現場ではこれまでにいくつもの取組みを実施してきました。 たとえば、運賃計算ソフトウェアのテストの品質を向上するために、テストパターンの設計方法およびテスト実行方法の改善についての取り組みがあります。 ICカードを改札機にタッチしたときの乗車駅・降車駅・定期券の経路などの組合せのパターンは10の40乗を超えますが、「不具合は漏らさないが実行可能な規模のテストパターン」への絞り込みを自動的に行い、数百万件規模のテストを効率的に実行しています。 また、現状の仕様書の記述上の問題点を払拭するために、運賃計算ソフトウェアの計算ルールの仕様書を形式仕様記述言語を利用して書きなおし、内在する問題点を明らかにしました。 本講演では、これらの取組みの詳細について紹介いたします。
11:15 - 12:00 セッション8  最適化  (座長 : 馬谷 誠二 (京都大学))
科学技術計算における最適化に伴う分割の正しさを検査するユニットテストフレームワーク HPCUnit [C1]
穂積 俊平 (東京大学), 佐藤 芳樹 (東京大学), 千葉 滋 (東京大学)
Answer Set Programming as a Modeling Language for Course Timetabling [C2]
Mutsunori Banbara (Kobe University), Takehide Soh (Kobe University), Naoyuki Tamura (Kobe University), Katsumi Inoue (National Institute of Informatics), Torsten Schaub (University of Potsdam)

2日目 (3月6日) 午後の部

13:10 - 14:20 セッション9  計算モデルと意味論  (座長 : 中澤 巧爾 (京都大学))
Parametric Effect Monads and Semantics of Effect Systems [C2]
Shin-ya Katsumata (Kyoto University)
Neighborhood-Sheaf Semanticsによる 一階述語条件論理の意味論 [C1]
山本 華子 (お茶の水女子大学), 戸次 大介 (国立情報学研究所, 科学技術振興機構 CREST)
限定継続を用いたフォーカスの分析と実装 [C1]
叢 悠悠 (お茶の水女子大学), 浅井 健一 (お茶の水女子大学), 戸次 大介 (お茶の水女子大学)
14:30 - 15:45 セッション10  項書換え系  (座長 : 小川 瑞史 (北陸先端科学技術大学院大学))
閉包操作に基づく右基底項書き換えシステムの到達可能性判定 [C1]
四方 駿作 (東北大学), 青戸 等人 (東北大学), 外山 芳人 (東北大学)
永続性と減少ダイアグラム法に基づく合流性自動証明 [C1]
内田 和真 (東北大学), 青戸 等人 (東北大学), 外山 芳人 (東北大学)
名目書き換えシステムの合流性について [C1]
鈴木 貴樹 (東北大学), 菊池 健太郎 (東北大学), 青戸 等人 (東北大学), 外山 芳人 (東北大学)
15:55 - 16:40 セッション11  高精度計算  (座長 : 勝股 審也 (京都大学))
Improving Floating-Point Numbers: a Lazy Approach to Adaptive Accuracy Refinement for Numerical Computations [C1]
Hideyuki Kawabata (Hiroshima City University), Hideya Iwasaki (The University of Electro-Communications)
A Stream Calculus of Bottomed Sequences for Real Number Computation [C2]
Kei Terayama (Kyoto University), Hideki Tsuiki (Kyoto University)
16:50 - 18:00 セッション12  関数型プログラミング言語  (座長 : Jacques Garrigue (名古屋大学))
Mio: A High-Performance Multicore IO Manager for GHC [C2]
Andreas Voellmy (Yale University), Junchang Wang (Yale University), Paul Hudak (Yale University), Kazuhiko Yamamoto (IIJ Innovation Institute Inc.)
型デバッガのログの解析とエラーメッセージの改良 [C1]
石井 柚季 (お茶の水女子大学), 浅井 健一 (お茶の水女子大学)
Enumerating Counter-Factual Type Error Messages with an Existing Type [C1]
Kanae Tsushima (Kyoto University), Olaf Chitil (University of Kent)

2日目 (3月6日) 夜の部

20:00 - 22:00 セッション13  ポスター・デモ (2)  
CoqからScalaへのロバストなコード抽出 [C3]
逸見 港 (東京大学), 田辺 良則 (国立情報学研究所), 萩谷 昌己 (東京大学)
A Practical Study of MapReduce on Supercomputers [C3]
Thanh-Chung Dao (東京大学), Shigeru Chiba (東京大学)
高階モデル検査による高階並行プログラムの同時到達可能性の解析 [C3]
安酸 円秀 (東京大学), 小林 直樹 (東京大学), 松田 一孝 (東京大学)
越段階埋込とプログラム生成 [C3]
花田 裕一朗 (京都大学), 五十嵐 淳 (京都大学)
MapReduce フレームワークにおける Combiner の自動生成 [C3]
樹下 稔 (京都大学), 末永 幸平 (京都大学), 五十嵐 淳 (京都大学)
外延的Λμ計算の簡約体系 [C3]
中澤 巧爾 (京都大学), 永井 智映 (京都大学)
契約つきモジュール計算のトレース意味論に向けて [C3]
村井 涼 (京都大学), 五十嵐 淳 (京都大学), 中澤 巧爾 (京都大学)
Java Native Interface におけるアクセス制御違反を検出するツールの開発 [C3]
宮岡 大騎 (電気通信大学), 岩崎 英哉 (電気通信大学)
LuaとCを混在して記述できる言語の提案 [C3 (デモ)]
谷村 明 (電気通信大学), 岩崎 英哉 (電気通信大学)
イベント駆動方式サーバのための並列JavaScript処理系の実装 [C3]
藤井 亮太 (電気通信大学), 岩崎 英哉 (電気通信大学), 中野 圭介 (電気通信大学), 鵜川 始陽 (電気通信大学)
Extending event-driven programming to support reactive programming by adding an inference mechanism (continued) [C3]
莊 永裕 (東京大学), 千葉 滋 (東京大学)
言語機構の有用性の定量的な評価のためのクエリ言語の開発に向けて [C3]
小川 秀典 (東京大学)
Interfaces for Separate Compilation of Aspect-Oriented Programs with Inter-Type Declarations [C3]
当山 学 (東京大学), 青谷 知幸 (東京工業大学), Eric Bodden (EC SPRIDE, Technische Universitaet Darmstadt), 増原 英彦 (東京工業大学), Eric Tanter (Universidad de Chile)
スケジューラを用いた量子プロセス間の観測同値 [C3]
安田 和矢 (東京大学), 久保田 貴大 (東京大学), 角谷 良彦 (東京大学)
Improving SequenceライブラリのScalaにおける実装 [C3]
山本 竜太郎 (電気通信大学), 岩崎 英哉 (電気通信大学)
OCamlにおける多相関数の複製の実験 [C3 (デモ)]
徳田 亮平 (東北大学), 住井 英二郎 (東北大学)
OCamlにおけるセッション型のエンコードと型推論 [C3]
今井 敬吾 (京都大学), 結縁 祥治 (名古屋大学)
タスク並列言語Tascellを用いたアイテム共有部分グラフの並列マイニング [C3]
奥野 伸吾 (京都大学), 平石 拓 (京都大学), 中島 浩 (京都大学), 八杉 昌宏 (九州工業大学), 瀬々 潤 (東京工業大学)
Towards demand-oriented study for program synthesis [C3]
大平 怜 (日本IBM東京基礎研究所), 林崎 弘成 (日本IBM東京基礎研究所)
A Tree-Decomposition Based Approach to Target Set Selection Problem [C3 (デモ)]
劉 雨 (総合研究大学院大学), 胡 振江 (国立情報学研究所)
アスペクト指向アルゴリズムアニメーションフレームワーク [C3]
邵 冰峰 (東京大学), 増原 英彦 (東京工業大学), 青谷 知幸 (東京工業大学), 当山 学 (東京大学)
型安全なシェルプログラミングのための領域特化言語の提案 [C3]
朝倉 泉 (東京工業大学), 増原 英彦 (東京工業大学), 青谷 知幸 (東京工業大学)
shift/reset とカリーハワード同型 [C3]
上田やよい (お茶の水女子大学), 浅井健一 (お茶の水女子大学)

3日目 (3月7日) 午前の部

8:45 - 10:00 セッション14  コンパイラ  (座長 : 大平 怜 (日本IBM))
構文主導型値グラフ構築 [C1]
佐藤 重幸 (電気通信大学)
質問伝播に基づくスカラー置換 [C1]
澄川 靖信 (東京理科大学), 小島 量 (管理工学研究所), 滝本 宗宏 (東京理科大学)
サーバサイド向け JavaScript 処理系における Just In Time コンパイラの実装 [C1]
漆原 明博 (電気通信大学), 岩崎 英哉 (電気通信大学), 鵜川 始陽 (電気通信大学)
10:10 - 11:00 セッション15  メタプログラミング  (座長 : 五十嵐 淳 (京都大学))
MetaOCaml を使った自己反映言語のコンパイル [C1]
浅井 健一 (お茶の水女子大学)
ドメイン特化言語処理系実装支援ライブラリのメタプログラミングによる実現 [C1]
塩田 雅人 (電気通信大学), 岩崎 英哉 (電気通信大学)
11:10 - 12:15 セッション16  オートマトンとアルゴリズム  (座長 : 南出 靖彦 (筑波大学))
Well-Structured Pushdown Systems [C2]
Xiaojuan Cai (Shanghai Jiao Tong University), Mizuhito Ogawa (Japan Advanced Institute of Science and Technology)
Nested Timed Automata [C2]
Guoqiang Li (Shanghai Jiao Tong University), Xiaojuan Cai (Shanghai Jiao Tong University), Mizuhito Ogawa (Japan Advanced Institute of Science and Technology), Shoji Yuen (Nagoya University)
漸増計算法の第三リスト準同型定理による系統的導出 [C1]
森畑 明昌 (東北大学)
12:15 - 12:45 クロージング

NOTICE     PPL aims to function as an informal workshop series, which gives researchers an opportunity to disseminate their preliminary work and get feedback from the participants without precluding publication elsewhere. It encourages submissions of revised versions of the work to international conferences or refereed journals.
    The second category of PPL ([C2] in the program above) is intended to help researchers disseminate their research to the domestic community by providing an opportunity to present their papers that have already been accepted by international conferences or journals (but not presented in Japan before). Therefore, presentations in this category, which are informal, should not be considered republication or results of double submissions of any kind.


_戻る