Theory of Higher-Order Typed Programs based Software Contracts

2016 Fiscal Year Final Research Report

• 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: Igarashi Atsushi 京都大学, 情報学研究科, 教授 (40323456)
• Co-Investigator(Kenkyū-buntansha): 馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831) ; 末永 幸平 京都大学, 情報学研究科, 准教授 (70633692) ; 中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
• Project Period (FY): 2013-04-01 – 2017-03-31
• Keywords: プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / トレース意味論 / 代入 / 限定継続

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.

Free Research Field

プログラミング言語