PMAN - Paper management system: 大久保弘崇, 山本晋一郎, 坂部俊樹, 稲垣康善, モデル生成法に基づくJavaScriptプログラム型検査の機械実行, 2006年4月.
Detail of a work
| Tweet | |
| 大久保弘崇, 山本晋一郎, 坂部俊樹, 稲垣康善, "モデル生成法に基づくJavaScriptプログラム型検査の機械実行," 電子情報通信学会論文誌, J89-D(4), pp. 693-704 2006年4月. | |
| ID | 22 |
| 分類 | 論文誌 |
| タグ | |
| 表題 (title) |
モデル生成法に基づくJavaScriptプログラム型検査の機械実行 |
| 表題 (英文) |
|
| 著者名 (author) |
大久保弘崇,山本晋一郎,坂部俊樹,稲垣康善 |
| 英文著者名 (author) |
|
| キー (key) |
|
| 定期刊行物名 (journal) |
電子情報通信学会論文誌 |
| 定期刊行物名 (英文) |
|
| 巻数 (volume) |
J89-D |
| 号数 (number) |
4 |
| ページ範囲 (pages) |
693-704 |
| 刊行月 (month) |
4 |
| 出版年 (year) |
2006 |
| Impact Factor (JCR) |
|
| URL |
|
| 付加情報 (note) |
|
| 注釈 (annote) |
論文は http://www.aichi-pu.ac.jp/ist/~ohkubo/study.ja.html を参照してください |
| 内容梗概 (abstract) |
プログラムの実行の安全性を保証するために，プログラムに対する型検査がしばしば行われる．本論文では，型のないオブジェクト指向言語である JavaScript で書かれたプログラムの型検査について述べる．本論文の型検査は，型規則を形式的な推論規則で記述し，これを自動証明系で直接実行するアプローチを特徴とする．この方法により，型検査系の実装時の誤りがなく正確な型検査が行え，また型検査系の構築・拡張が形式的な枠組みに基づいて行える．自動証明系には MGTP を用いた．MGTP はモデル生成法に基づく証明系で，推論規則の記述が直観的に行える．本論文では，推論規則によって定式化した型検査系をMGTP により自動証明可能な形式で表現する方法を示す．この際，推論規則には現れない暗黙の条件である型整合性の検査規則を明示する必要があることを明らかにし，またそれをMGTP 規則で表現する際の手法について述べる． キーワードJavaScript, 型検査, 定理自動証明, MGTP |
| 論文電子ファイル | 利用できません． |
| BiBTeXエントリ |
@article{id22,
title = {モデル生成法に基づくJavaScriptプログラム型検査の機械実行},
author = {大久保弘崇 and 山本晋一郎 and 坂部俊樹 and 稲垣康善},
journal = {電子情報通信学会論文誌},
volume = {J89-D},
number = {4},
pages = {693-704},
month = {4},
year = {2006},
annote = {論文は http://www.aichi-pu.ac.jp/ist/~ohkubo/study.ja.html を参照してください},
}
|