2017 Fiscal Year Final Research Report
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
|
| 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.
|
| Free Research Field |
プログラミング言語論、関数プログラミングと方システム、プログラム生成、定理証明
|
