ICE-based refinement type discovery for higher-order functional programs

Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

13 被引用数 (Scopus)

抄録

We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine learning, their Ice framework uses implication constraints, which consist of pairs (x, y) such that if x satisfies an invariant, so does y. From these constraints, Ice infers inductive invariants effectively. We observe that the implication constraints in the original Ice framework are not suitable for finding invariants of recursive functions with multiple function calls. We thus generalize the implication constraints to those of the form ((x1, ⋯, xk), y), which means that if all of x1, ⋯, xk satisfy an invariant, so does y. We extend their algorithms for inferring likely invariants from samples, verifying the inferred invariants, and generating new samples. We have implemented our method and confirmed its effectiveness through experiments.

本文言語英語
ホスト出版物のタイトルTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
編集者Dirk Beyer, Marieke Huisman
出版社Springer Verlag
ページ365-384
ページ数20
ISBN(印刷版)9783319899596
DOI
出版ステータス出版済み - 1 1 2018
イベント24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 - Thessaloniki, ギリシャ
継続期間: 4 14 20184 20 2018

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
10805 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

その他

その他24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Countryギリシャ
CityThessaloniki
Period4/14/184/20/18

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「ICE-based refinement type discovery for higher-order functional programs」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル