POPLmarkチャレンジ

プログラミング言語理論において、POPLmark チャレンジ(「Principles of Programming Languages benchmark」に由来、以前はMechanized Metatheory for the Masses! と呼ばれていた) (Aydemir、2005) は、プログラミング言語のメタ理論における自動推論(または機械化)の状態を評価し、形式手法コミュニティのさまざまな分野の間で議論とコラボレーションを促進するために設計された一連のベンチマークです。大まかに言えば、このチャレンジは、プログラムが意図された動作の仕様にどれだけ適合しているかを実証できるか (およびこれに伴う多くの複雑な問題) を測定することです。このチャレンジは、当初、ペンシルバニア大学のPL クラブのメンバーが世界中の協力者と共同で提案しました。Mechanized Metatheory に関するワークショップは、このチャレンジに参加する研究者の主な会議です。

POPLmark ベンチマークの設計は、プログラミング言語に関する推論に共通する特徴に基づいています。チャレンジ問題では、大規模なプログラミング言語の形式化は必要ありませんが、以下の点について推論する高度な知識が必要です。

バインディング: ほとんどのプログラミング言語には何らかの形式のバインディングがあり、その複雑さは、単純に型付けされたラムダ計算の単純なバインダーから、レコードパターンの処理に必要な複雑で潜在的に無限のバインダーまで多岐にわたります。
誘導: 主語の縮小や強い正規化などの特性には、複雑な帰納的議論が必要になることがよくあります。
再利用: コラボレーションの促進がこのチャレンジの主要目的であるため、ソリューションには再利用可能なコンポーネントが含まれることが期待されており、研究者は毎回ゼロから始めることなく言語機能と設計を共有できるようになります。

問題点

2007 年現在^[update]、 POPLmark チャレンジは 3 つのパートで構成されています。パート 1 はSystem F _<: (サブタイプを持つSystem F ) の型のみを対象としており、次のような問題があります。

型システムがサブタイプの推移性を認めているかどうかを確認します。
レコードが存在する場合のサブタイプの推移性をチェックする

_{第2部では、System F <:}の構文と意味について扱います。

純粋なフラグメントの型安全性
パターンマッチングがある場合の型安全性

_{パート 3 は、System F <:}の形式化の有用性に関するものです。特に、課題では次のことが求められます。

操作意味論のシミュレーションとアニメーション化
形式化から有用なアルゴリズムを抽出する

POPLmark チャレンジの一部には、Isabelle/HOL、Twelf、Coq、 αProlog 、ATS、 Abella 、Matitaなどのツールを使用したいくつかのソリューションが提案されています。

参照

参考文献

Brian E. Aydemir、Aaron Bohannon、Matthew Fairbairn、J. Nathan Foster、Benjamin C. Pierce、Peter Sewell、Dimitrios Vytiniotis、Geoffrey Washburn、Stephanie C. Weirich、Stephan A. Zdancewic。「大衆向けの機械化されたメタ理論：POPLmark の挑戦」。「Theorem Proving in Higher Order Logics」、第 18 回国際会議、TPHOLs 2005、Lecture Notes in Computer Science の第 3603 巻、50 ～ 65 ページ。Springer、ベルリン/ハイデルベルク/ニューヨーク、2005 年。
Benjamin C. Pierce、Peter Sewell、Stephanie Weirich、Steve Zdancewic、「プログラミング言語メタ理論を機械化する時が来た」、Bertrand Meyer、Jim Woodcock (編) Verified Software: Theories, Tools, Experiments、LNCS 4171、Springer Berlin / Heidelberg、2008、pp. 26–30、ISBN 978-3-540-69147-1

外部リンク

POPLmarkチャレンジ