Detail of a work
Tweet | |
大久保弘崇, 山本晋一郎, 坂部俊樹, 稲垣康善, "形式的手法に基づく JavaScriptプログラムの型検査系の実現," 信学技報, 104(47(ISSN 0913-5685)), pp. 13--18 2004年5月. | |
ID | 19 |
分類 | 研究会・全国大会等 |
タグ | |
表題 (title) |
形式的手法に基づく JavaScriptプログラムの型検査系の実現 |
表題 (英文) |
|
著者名 (author) |
大久保弘崇,山本晋一郎,坂部俊樹,稲垣康善 |
英文著者名 (author) |
|
編者名 (editor) |
|
編者名 (英文) |
|
キー (key) |
|
書籍・会議録表題 (booktitle) |
信学技報 |
書籍・会議録表題(英文) |
|
巻数 (volume) |
104 |
号数 (number) |
47(ISSN 0913-5685) |
ページ範囲 (pages) |
13--18 |
組織名 (organization) |
|
出版元 (publisher) |
|
出版元 (英文) |
|
出版社住所 (address) |
|
刊行月 (month) |
5 |
出版年 (year) |
2004 |
採択率 (acceptance) |
|
URL |
|
付加情報 (note) |
会津大学, SIGSS |
注釈 (annote) |
|
内容梗概 (abstract) |
我々は,形式的手法の実際的応用を目指し,次の3つの視点から研究を進めている.第1は,型のないオブジェクト指向言語であるJavaScriptに対する型検査手法を提案すること.この型検査により,JavaScriptプログラムの安全性を高めることができる.第2は,ソフトウェア工学の問題に汎用の定理証明系を適用することにより,形式的手法を現実的な問題に直接適用する可能性を探ること.このため,型検査系を推論規則により形式的に定義し,これを極力そのままの形で実際のプログラムに適用する.第3は,上の目的に適合する定理証明系のための言語を提案すること.ソフトウェア工学の現実的な問題に定理証明系を適用する際に必要となるシンタックスシュガーや演算定義能力についての知見を得る.本稿では,JavaScriptのサブセット言語に対する単純な型推論系に基づいて,モデル生成型の定理証明系による自動証明による型検査を試みる. キーワード JavaScript, 型検査, 推論系 |
論文電子ファイル | 3.pdf (application/pdf) [一般閲覧可] |
BiBTeXエントリ |
@inproceedings{id19, title = {形式的手法に基づく JavaScriptプログラムの型検査系の実現}, author = {大久保弘崇 and 山本晋一郎 and 坂部俊樹 and 稲垣康善}, booktitle = {信学技報}, volume = {104}, number = {47(ISSN 0913-5685)}, pages = {13--18}, month = {5}, year = {2004}, note = {会津大学, SIGSS}, } |