文脈計算の環境計算による解釈
スポンサーリンク
概要
- 論文の詳細を見る
本研究では, プログラミング言語における文脈と環境の関係を調べる.プログラミング言語において文脈とは, 穴を持つプログラムのことである.文脈はプログラミング言語の操作的意味論を定義するときなどに用いられる.橋本, 大堀(1996)は文脈をファーストクラスのオブジェクトとして持つ型付きλ計算を考えた.ファーストクラスの文脈を用いて, モジュールシステムやモバイルコードを柔軟に扱うことができると期待されている.一方, プログラミング言語において環境とは, 変数の名前とその値の組の集合のことである.環境は局所的束縛を扱うためにしばしば用いられる.LISPのletなどは環境を作り, その中でプログラムを評価するものである.環境をファーストクラスのオブジェクトとして持つようなλ計算はいくつかあり, 佐藤, Burstall, 桜井(1999)によるλεはその1つである.ファーストクラスの環境を用いてオブジェクト指向プログラミングなどを扱うことができると期待されている.本研究では, 橋本, 大堀の型付文脈計算を, 佐藤, Burstall, 桜井のλεを用いて解釈し, 解釈の健全性を証明した.また, これにより型付文脈計算が強正規性を満たすことが分かった.
- 一般社団法人情報処理学会の論文
- 2000-11-15
著者
関連論文
- モデル検査を用いたタグVLANの設定検査(ネットワークサービス基礎)
- タグスイッチネットワークのモデル検査による漏曳検査(セッション3)
- SET支払いプロトコルの秘匿性検証(セキュリティプロトコル・電子公証)(新たな脅威に立ち向かうコンピュータセキュリティ技術)
- ゲーム列による安全性証明の形式化と自動化(数理的技法による情報セキュリティ)
- 関数部分知識と匿名性検証(理論,数理的技法による情報セキュリティ,平成19年研究部会連合発表会)
- 攻撃者を考慮した匿名性検証法 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (形式的手法)
- プロセス代数を用いたセキュリティ・プロトコル記述
- 文脈計算の環境計算による解釈
- 電子投票プロトコルに対する無証拠性の定理証明
- フォーマルメソッドによるセキュリティ&プライバシ (特集 20周年を迎えたコミュニケーション科学)
- 電子投票プロトコルに対する無証拠性の定理証明 (特集 人と共存するコンピュータセキュリティ技術)