POPL2013, PEPM2013, PLMW2013報告
POPL2013
POPL はプログラミング言語理論に
関する最高峰の国際会議のひとつである．とはいって
も，少くとも昨今では，純粋に理論的な論文はむしろ
少なく，現実の問題に対する理論に基づくアプローチ
という論文のほうが多い印象である．
The Sequential Semantics of Producer Effect Systems
effectの意味論の枠組み, “productor”
- effect: 入力と出力の値とは独立した計算の分類
- ex. 入力を捨てる
- 入力をどう消費するかのeffect: consumer
- 計算結果に伴うeffect: ex. 出力の代わりに例外を返すかもしれない
Copatterns: Programming Infinite Structures by Observations
infinite object に対するpatternである copattern
Coq では, 無限の構造として, コンストラクタで余帰納的(coninductive)な型を定義出来るが,
- 強正規化が必要
- subject reduction を満たさなくなる
という問題が合ったが, 克服した.
Checking NFA Equivalence with Bisimulations up to Congruence
NFA の等価性判定に対して新たなアルゴリズムを提案
決定化されたオートマトンで, 状態 , それが受理する言語 に対し, から探索空間を減らした.
- 古典的な Hopcroft, Karpアルゴリズム
- antichainアルゴリズム
に比べ顕著に高速
実はこの提案手法の特殊系が antichainアルゴリズム だった.
PEPM2013
プログラム変換を中心としたプログラム操作技術に
フォーカスをおいた専門的な国際ワークショップ
bidirectional transformation
: あるデータからデータへの順方向の変換と逆方向の変換の組
Partially Static Operations
演算子の代数的性質を利用した数値の部分計算.
ex.
(a + b) + (c + d) で, a = 100, b = 20, d = 3 がわかっていた時, 120 + (c + 3) であるが, 加算の結合性と可換性を用いて, ((a + b) + d) + c と書き換えられれば, 123 + c となりより効果的に部分計算を行える.
このような演算を partially static operations という.
PLMW2013
学部生や大学
院生を対象とするメンタリングワークショップであ
り，昨年から開催されている．プログラミング言語分
野の最先端の研究や，研究者としてのキャリアの築
き方を紹介し，この分野への進学奨励や研究奨励を
目的としている．
Program Logic and Analysis
FloydのAssigning Meanings to Programsまでさかのぼり, ホーア論理 を説明して, 自動化されたプログラム検証器を紹介していた.
Calculi, Processes, Coinduction
計算・プロセス・余帰納法のそれぞれの研究の動機を説明し，双模倣性や帰納法と余帰納法の双対性，さらにこの研究分野における現在の課題などが紹介された.
Computational Trinitarianism
プログラミング言語研究における 型理論，証明論，圏論 の 3 理論の「三位一体説」の重要性が説かれ，証明の計算や等価性について説明
された.