Design and development of multi-stage languages for verification
| Project/Area Number |
15K12007
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
|
|---|
| Research Collaborator |
SAKAGUCHI Kazuhiko 筑波大学, システム情報工学研究科
WATANBE Takahisa 筑波大学, システム情報工学研究科
OISHI Jumpei 筑波大学, システム情報工学研究科
USUI Chiharu 筑波大学, システム情報工学研究科
SUDO Yuto 筑波大学, システム情報工学研究科
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2015: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 証明記述言語 / プログラム生成 / メタプログラミング / コントロールエフェクト / 副作用 / 型安全性 / モジュール / 定理証明支援システム / プログラム抽出・生成 / 型システム / スコープ安全性 / 定理証明系 / 形式検証 / 証明の自動化 / プログラム抽出 / 証明探索 / 証明の生成 |
|---|
| Outline of Final Research Achievements |
This study aims at applying the method and results in metaprogrmaming to proof-description languages. Based on static assurance of generated code in terms of static typing for metaprograms, we enriched the expressiveness of code description languages by introducing mutable cells and delimited control. We have also extended the object language to ML-style modules. In both cases, we have successfully designed a type system which enjoy the soundness property, that implies that each generated code is scope safe and type safe. Using these results, we have designed a very simple proof-description language which allows side effects, and obtained a certain preliminary thoughts on proof generation using side effects.
|
Report
(4 results)
Research Products
(16 results)
