WEKO3
アイテム
定理証明器によるモジュラーなソフトウェア検証
https://tsurumi-u.repo.nii.ac.jp/records/1199
https://tsurumi-u.repo.nii.ac.jp/records/1199d91fae88-3567-444a-845b-f63325a5faaa
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
25330096 (264.6 kB)
|
.png)
|
| Item type | 報告書 / Research Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2022-04-20 | |||||
| タイトル | ||||||
| タイトル | 定理証明器によるモジュラーなソフトウェア検証 | |||||
| 言語 | ja | |||||
| タイトル | ||||||
| タイトル | Modular software verification with a proof assistant | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| キーワード | ||||||
| 言語 | ja | |||||
| 主題Scheme | Other | |||||
| 主題 | 定理証明支援系 | |||||
| キーワード | ||||||
| 言語 | ja | |||||
| 主題Scheme | Other | |||||
| 主題 | ソフトウェア検証 | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18ws | |||||
| 資源タイプ | research report | |||||
| 研究代表者 |
田辺, 良則
× 田辺, 良則 |
|||||
| 報告年度 | ||||||
| 日付 | 2016-03-31 | |||||
| 日付タイプ | Issued | |||||
| 研究課題番号 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 研究課題/領域番号 : 25330096 | |||||
| 言語 | ja | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 研究成果の概要（和文）：定理証明支援系Coqから，プログラミング言語Scalaへのコード抽出を実現した．Coqによって，コードが正しく動作することの証明を記述した上でコード抽出をすれば，抽出されたコードの正しさが保証される．Scalaコードは，Javaで記述された多数のシステムと親和性が高いと期待される．コード抽出を行うコード自体もCoqで記述されており，その動作が妥当であることが，Coq上の証明として与えられている． | |||||
| 言語 | ja | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 研究成果の概要（英文）：We have implemented code extraction from proof assistant Coq to programming language Scala. Once a proof is given to a code written in Coq, then the extracted code is guaranteed that it behaves correctly. There are many working systems written in Java, and Scala code is easily integrated with them because it runs on Java VM. Our code itself is originally written in Coq and is extracted from a proof on Coq that it works correctly. | |||||
| 言語 | en | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・2015(平成27)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 | |||||
| 言語 | ja | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・研究期間 (年度)：2013-04-01 – 2016-03-31 | |||||
| 言語 | ja | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | ・研究分野：情報理工学 | |||||
| 言語 | ja | |||||
| 関連サイト | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-25330096/ | |||||
| 著者版フラグ | ||||||
| 出版タイプ | AM | |||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
