Refinement Type Checking via Assertion Checking

• Item type: Trans(1)
• 公開日: 2015-09-21
• タイトル: Refinement Type Checking via Assertion Checking
• タイトル / 言語: en
• タイトル: Refinement Type Checking via Assertion Checking
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] refinement types, assertion checking, automated verification
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属: Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属: Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者名: Ryosuke, Sato; Kazuyuki, Asada; Naoki, Kobayashi
• 著者名(英): Ryosuke, Sato; Kazuyuki, Asada; Naoki, Kobayashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 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.; \n------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.23(2015) No.6(online); ------------------------------
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.; \n------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.23(2015) No.6(online); ------------------------------
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 8, 号 3, 発行日 2015-09-21
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会