Theory of Higher-Order Typed Programs based Software Contracts
| Project/Area Number |
25280024
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Partial Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥18,070,000 (Direct Cost: ¥13,900,000、Indirect Cost: ¥4,170,000)
Fiscal Year 2015: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
Fiscal Year 2014: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
Fiscal Year 2013: ¥6,890,000 (Direct Cost: ¥5,300,000、Indirect Cost: ¥1,590,000)
|
|---|
| Keywords | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / トレース意味論 / 代入 / 限定継続 / ゲーム意味論 / shift/reset |
|---|
| Outline of Final Research Achievements |
We studied the integration of computational effects such as delimited continuatios and mutable state and software contracts; we proposed a contract calculus and a blame calculus with delimited continuations and a manifest contract calculus with mutable state and proved their desirable properties. We proposed an extension of a manifest contract calculus with algebraic datatypes; we compared two styles of specification for datatypes and showed that a contract written in one style can be reduced to the other without changing its meaning in a certain sense. We extended OCaml to implement manifest contracts for datatypes. Finally, we studied trace semantics for a contract calculus as denotational semantics of software contracts.
|
Report
(5 results)
Research Products
(41 results)
-
-
-
-
-
-
-
-
-
[Journal Article] Manifest Contracts for Datatypes2015
Author(s)
Taro Sekiyama, Yuki Nishida, Atsushi Igarashi
-
Journal Title
Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Volume: 1
Pages: 195-207
DOI
Related Report
Peer Reviewed / Acknowledgement Compliant
-
-
-
-
-
-
-
[Presentation] Stateful manifest contracts2017
Author(s)
Taro Sekiyama, Atsushi Igarashi
Organizer
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Place of Presentation
フランス・パリ
Year and Date
2017-01-18
Related Report
Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] Manifest Contracts for Datatypes2015
Author(s)
Taro Sekiyama, Yuki Nishida, Atsushi Igarashi
Organizer
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Place of Presentation
Mumbai, India
Year and Date
2015-01-15 – 2015-01-17
Related Report
-
-
-
-
-
-
-
-
-
-
-
-
