研究会名：コンピュータサイエンス研究会　講演会
開催日：2009年5月8日 （金）15:00～16:00
題目：プログラム理論演習システムのための “Prelogical” Framework とその実装
講師：五十嵐 淳氏（京都大学）
開催場所：東北大学電気情報系3号館206号室

コンピュータサイエンス研究会 講演会の御案内

コンピュータサイエンス研究会
主査 小林直樹

下記のようにコンピュータサイエンス研究会の講演会を開催いたしますので，ご案内申し上げます．

なお，講演者の五十嵐氏は，（今回の講演内容は受賞とは直接の関係はありませんが）第1回「マイクロソフトリサーチ日本情報学研究賞」の受賞者に決定しております．

• 日時：2009年5月8日（金）15:00～16:00
• 場所：東北大学 電気情報系3号館 206号室
• 題目：プログラム理論演習システムのための “Prelogical” Framework とその実装
• 話者：五十嵐 淳氏（京都大学）
• 概要：講演者が京都大学で行っているプログラム理論(主に core MLの操作的意味論・型システム)に関する大学院講義「ソフトウェア基礎論」のための演習システムの設計と実装について概説する．演習システムは，学生が入力した具体的なMLプログラムの評価や型付けの導出を検査し正誤を返すCGIプログラムである．導出の正しさの検査をする部分はOCamlで書かれているが，これは推論規則や抽象構文定義を含む体系記述から自動的に生成されている．自動生成をする理由は，講義の進度に応じて拡大・修正されていく対象言語ひとつひとつについて導出検査器を手で作成するのは手間がかかり誤りが混入しやすいためである．我々は，形式体系記述のためのメタ言語Prelog(仮称)を設計し，導出検査器を自動生成するコンパイラを作成した．Prelogの特徴は，推論規則中でOCaml関数によって実装された述語を使用できることにある．これにより，非形式的に記述される付帯条件を簡単に表現することができる．