計算機言語論第8回

🍣 @nin_ten

今日から後半 #計算機言語論

XENO @xenophobia__

スライドか…… #計算機言語論

🍣 @nin_ten

エアコン効いてる #計算機言語論

🍣 @nin_ten

高階モデル検査 #計算機言語論

XENO @xenophobia__

"Automata, Logics, and Infinite Games" Springer LNCS 2500 #計算機言語論

XENO @xenophobia__

じゃあメモらずに話をちゃんと聞く方向でいいのか #計算機言語論

ネクタイ @carbon_twelve

成績はレポート。出席は無し。 #計算機言語論

XENO @xenophobia__

研究室紹介14:15から #計算機言語論

ネクタイ @carbon_twelve

高階モデル検査って何に使えるの？っていう話を #計算機言語論

XENO @xenophobia__

高階モデル検査とは #計算機言語論

ネクタイ @carbon_twelve

higher-order recursion scheme #計算機言語論

ネクタイ @carbon_twelve

非終端記号が木に関する高階関数を引数に取れる #計算機言語論

XENO @xenophobia__

この辺、前とnotation違ってるな #計算機言語論

ネクタイ @carbon_twelve

無限木を生成するための高階関数プログラムだと思える #計算機言語論

ネクタイ @carbon_twelve

「全ての有限パスはcで終わるか？」とか「bの後にaが現れるか？」とかといった質問に答えるのが高階モデル検査 #計算機言語論

ネクタイ @carbon_twelve

決定可能ではあるが、k-EXPTIME完全 #計算機言語論

ネクタイ @carbon_twelve

他のモデルとの対応 #計算機言語論

ネクタイ @carbon_twelve

簡単な歴史 #計算機言語論

ネクタイ @carbon_twelve

高階モデル検査の応用 #計算機言語論

XENO @xenophobia__

高階モデル検査器の実用的な実装が与えられたのは2009年 #計算機言語論

XENO @xenophobia__

プログラムをCPS変換によって高階再帰スキームに変換する #計算機言語論

ネクタイ @carbon_twelve

高階モデル検査のアルゴリズム #計算機言語論

ネクタイ @carbon_twelve

型検査の問題に帰着させる #計算機言語論