Refinement type checking via assertion checking

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

研究成果: Article査読

2 被引用数 (Scopus)

抄録

A refinement type can be used to express a detailed specification of a higher-order functional program. Given a refinement type as a specification of a program, we can verify that the program satisfies the specification by checking that the program has the refinement type. Refinement type checking/inference has been extensively studied and a number of refinement type checkers have been implemented. Most of the existing refinement type checkers, however, need type annotations, which is a heavy burden on users. To overcome this problem, we reduce a refinement type checking problem to an assertion checking problem, which asks whether the assertions in a program never fail; and then we use an existing assertion checker to solve it. This reduction enables us to construct a fully automated refinement type checker by using a state-of-the-art fully automated assertion checker. We also prove the soundness and the completeness of the reduction, and report on implementation and preliminary experiments.

本文言語English
ページ(範囲)827-834
ページ数8
ジャーナルJournal of information processing
23
6
DOI
出版ステータスPublished - 2015 11月 15
外部発表はい

ASJC Scopus subject areas

  • コンピュータ サイエンス(全般)

フィンガープリント

「Refinement type checking via assertion checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル