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: Igarashi Atsushi 京都大学, 情報学研究科, 教授 (40323456)
• Co-Investigator(Kenkyū-buntansha): 馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831) ; 末永 幸平 京都大学, 情報学研究科, 准教授 (70633692) ; 中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
• Project Period (FY): 2013-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥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.

Research Products

• [Int'l Joint Research] Pomona College(米国)
• [Int'l Joint Research] Pomona College(米国)
• [Journal Article] Polymorphic manifest contracts, Revised and Resolved (2017)
  • Author(s): Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg
  • Journal Title: ACM Transactions on Programming Languages and Systems Volume: 39 Issue: 1 Pages: 1-36
  • DOI: 10.1145/2994594
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Stateful manifest contracts (2017)
  • Author(s): Taro Sekiyama, Atsushi Igarashi
  • Journal Title: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Volume: - Pages: 530-544
  • DOI: 10.1145/3009837.3009875
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] An Extended Behavioral Type System for Memory-Leak Freedom (2016)
  • Author(s): Qi Tan, Kohei Suenaga, Atsushi Igarashi
  • Journal Title: 日本ソフトウェア科学会第33回大会論文集 Volume: -
  • NAID: 40021053614
  • Open Access
• [Journal Article] Shifting the Blame: A Blame Calculus with Static Delimited Control (2015)
  • Author(s): Taro Sekiyama, Soichiro Ueda, Atsushi Igarashi
  • Journal Title: Lecture Notes in Computer Science (Proceedings of Asian Symposium on Programming Languages and Systems) Volume: 9458 Pages: 189-207
  • DOI: 10.1007/978-3-319-26529-2_11
  • ISBN: 9783319265285, 9783319265292
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Manifest Contracts for OCaml (2015)
  • Author(s): Yuki Nishida, Atsushi Igarashi
  • Journal Title: Online Proceedings of ACM Workshop on ML Volume: -
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Design and Implementation of a Java Bytecode Manipulation Library for Clojure (2015)
  • Author(s): Seiji Umatani, Tomoharu Ugawa, Masahiro Yasugi
  • Journal Title: Journal of Information Processing Volume: 23 Issue: 5 Pages: 716-729
  • DOI: 10.2197/ipsjjip.23.716
  • NAID: 130005100079
  • ISSN: 1882-6652
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Manifest Contracts for Datatypes (2015)
  • 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: 10.1145/2676726.2676996
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] A Behavioral Type System for Memory-Leak Freedom (2015)
  • Author(s): Tan Qi, Kohei Suenaga, Atsushi Igarashi
  • Journal Title: 第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)論文集 Volume: 1
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] {高階契約を持つプログラミング言語に対するトレース意味論 (2015)
  • Author(s): 村井 涼, 中澤 巧爾, 五十嵐 淳
  • Journal Title: 第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)論文集 Volume: 1
• [Journal Article] Automatic Memory Management Based on Program Transformation using Ownerships (2014)
  • Author(s): Tatsuya Sonobe, Kohei Suenaga, Atsushi Igarashi
  • Journal Title: Lecture Notes in Computer Science (Proceedings of Asian Symposium on Programming Languages and Systems) Volume: 8858 Pages: 58-77
  • DOI: 10.1007/978-3-319-12736-1_4
  • ISBN: 9783319127354, 9783319127361
  • Peer Reviewed
• [Journal Article] 顕在的契約計算における代数的データ型 (2014)
  • Author(s): 関山太朗, 西田雄気, 五十嵐淳
  • Journal Title: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)オンライン論文集 Volume: 1 Pages: 1-18
  • Peer Reviewed
• [Journal Article] Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages (2014)
  • Author(s): Seiji Umatani
  • Journal Title: Proc. of ACM Symposium on Applied Computing Volume: 1 Pages: 1345-1351
  • Peer Reviewed
• [Presentation] A Type Reconstruction Algorithm for Gradually Typed Delimited Continuations (2017)
  • Author(s): Yusuke Miyazaki, Atsushi Igarashi
  • Organizer: 第19回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 山梨県笛吹市
  • Year and Date: 2017-03-08
• [Presentation] Stateful manifest contracts (2017)
  • 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
  • Int'l Joint Research
• [Presentation] An Extended Behavioral Type System for Memory-Leak Freedom (2016)
  • Author(s): Qi Tan and Kohei Suenaga, Atsushi Igarashi
  • Organizer: 日本ソフトウェア科学会第33回大会
  • Place of Presentation: 東北大学
  • Year and Date: 2016-09-06
• [Presentation] 限定継続演算子 shift/reset のための漸進的型付け (2016)
  • Author(s): 宮﨑 勇輔, 関山 太朗，五十嵐 淳
  • Organizer: 第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
  • Place of Presentation: ダイヤモンド瀬戸内マリンホテル(岡山県玉野市)
  • Year and Date: 2016-03-07
• [Presentation] A Denotational Semantics of a Probabilistic Stream-Processing Language (2016)
  • Author(s): Yohei Miyamoto, Kohei Suenaga, and Koji Nakazawa
  • Organizer: Workshop on Probabilistic Programming Semantics (PPS 2016)
  • Place of Presentation: St. Petersburg, FL, USA
  • Year and Date: 2016-01-23
  • Int'l Joint Research
• [Presentation] Gradual typing for delimited continuations (2016)
  • Author(s): Yusuke Miyazaki, Taro Sekiyama, Atsushi Igarashi
  • Organizer: International Workshop on Scripts to Programs
  • Place of Presentation: イタリア・ローマ
  • Int'l Joint Research
• [Presentation] Shifting the Blame: A Blame Calculus with Static Delimited Control (2015)
  • Author(s): Taro Sekiyama, Soichiro Ueda, Atsushi Igarashi
  • Organizer: 13th Asian Symposium on Programming Languages and Systems (APLAS2015)
  • Place of Presentation: Pohang, Korea
  • Year and Date: 2015-11-29
  • Int'l Joint Research
• [Presentation] Compositional Z: Confluence Proofs for Permutative Conversion (2015)
  • Author(s): Koji Nakazawa, Ken-etsu Fujita
  • Organizer: 第32回日本ソフトウェア科学会大会
  • Place of Presentation: 早稲田大学（東京都新宿区）
  • Year and Date: 2015-09-08
• [Presentation] Manifest Contracts for ML (2015)
  • Author(s): Yuki Nishida, Atsushi Igarashi
  • Organizer: ACM Workshop on ML
  • Place of Presentation: Vancouver, Canada
  • Year and Date: 2015-09-03
  • Int'l Joint Research
• [Presentation] Formal Verification of Software, Continuous, and Hybrid Systems – Or: How Do We Verify Our Program is Correct? (2015)
  • Author(s): Kohei Suenaga
  • Organizer: Machine Learning Summer School 2015
  • Place of Presentation: 京都大学（京都府京都市）
  • Year and Date: 2015-08-27
  • Int'l Joint Research / Invited
• [Presentation] Lambda Calculi and Confluence from A to Z (2015)
  • Author(s): Koji Nakazawa
  • Organizer: 4th International Workshop on Confluence (IWC2015)
  • Place of Presentation: Berlin, Germany
  • Year and Date: 2015-08-02
  • Int'l Joint Research / Invited
• [Presentation] Nonstandard Analysis Meets Programming Language Theory (2015)
  • Author(s): Kohei Suenaga
  • Organizer: The 12th International Conference on Computability and Complexity in Analysis (CCA 2015)
  • Place of Presentation: 明治大学(東京都千代田区）
  • Year and Date: 2015-07-13
  • Int'l Joint Research / Invited
• [Presentation] A Behavioral Type System for Memory-Leak Freedom (2015)
  • Author(s): Tan Qi, Kohei Suenaga, Atsushi Igarashi
  • Organizer: 第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)
  • Place of Presentation: 愛媛県松山市道後プリンスホテル
  • Year and Date: 2015-03-04 – 2015-03-06
• [Presentation] {高階契約を持つプログラミング言語に対するトレース意味論 (2015)
  • Author(s): 村井 涼, 中澤 巧爾, 五十嵐 淳
  • Organizer: 第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)
  • Place of Presentation: 愛媛県松山市道後プリンスホテル
  • Year and Date: 2015-03-04 – 2015-03-06
• [Presentation] Manifest Contracts for Datatypes (2015)
  • 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
• [Presentation] Automatic Memory Management Based on Program Transformation using Ownerships (2014)
  • Author(s): Tatsuya Sonobe, Kohei Suenaga, Atsushi Igarashi
  • Organizer: Asian Symposium on Programming Languages and Systems
  • Place of Presentation: Singapore
  • Year and Date: 2014-11-17 – 2014-11-19
• [Presentation] Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse (2014)
  • Author(s): Minoru Kinoshita, Kohei Suenaga, Atsushi Igarashi
  • Organizer: International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR2014)
  • Place of Presentation: Canterbury, UK
  • Year and Date: 2014-09-09 – 2014-09-11
• [Presentation] 顕在的契約計算における代数的データ型 (2014)
  • Author(s): 関山太朗, 西田雄気, 五十嵐淳
  • Organizer: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
  • Place of Presentation: 熊本県阿蘇市
• [Presentation] 型に基づく実行時契約検査機構の実装 (2014)
  • Author(s): 西田雄気, 関山太朗, 五十嵐淳
  • Organizer: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
  • Place of Presentation: 熊本県阿蘇市
• [Presentation] 限定継続を備えた計算体系へのソフトウェア契約の導入 (2014)
  • Author(s): 上田 宗一郎, 関山 太朗, 五十嵐 淳
  • Organizer: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
  • Place of Presentation: 熊本県阿蘇市
• [Presentation] 契約つきモジュール計算のトレース意味論に向けて (2014)
  • Author(s): 村井 涼, 五十嵐 淳, 中澤 巧爾
  • Organizer: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
  • Place of Presentation: 熊本県阿蘇市
• [Presentation] Practical Implementation Techniques of Ambient Calculus in Conventional Dynamic Languages (2014)
  • Author(s): Seiji Umatani
  • Organizer: ACM Symposium on Applied Computing
  • Place of Presentation: Gyeongju, Korea
• [Remarks] 五十嵐淳のホームページ
  • URL: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/
• [Remarks] 五十嵐淳のホームページ
  • URL: http://www.fos.kuis.kyoto-u.ac.jp
• [Remarks] 五十嵐淳のホームページ
  • URL: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/
• [Patent(Industrial Property Rights)] 不変条件生成装置，コンピュータプログラム，不変条件精製方法プロ グラムコード製造方法 (2016)
  • Inventor(s): 末永幸平，樹下稔，小島健介
  • Industrial Property Rights Holder: 京都大学
  • Industrial Property Rights Type: 特許
  • Industrial Property Number: 2016-017441
  • Filing Date: 2016-02-01
• [Patent(Industrial Property Rights)] 不変条件生成装置，コンピュータプログラム，不変条件生成方法，プログラムコード製造方法 (2016)
  • Inventor(s): 末永幸平，樹下稔，小島健介
  • Industrial Property Rights Holder: 京都大学
  • Industrial Property Rights Type: 特許
  • Industrial Property Number: 2016-017419
  • Filing Date: 2016-02-01