Refinement Types for Call-by-name Programs

• Item type: Trans(1)
• 公開日: 2023-08-28
• タイトル: Refinement Types for Call-by-name Programs
• タイトル / 言語: en
• タイトル: Refinement Types for Call-by-name Programs
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] Refinement types, Call-by-name programs, Automated verification
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: The University of Tokyo
• 著者所属(英): en
• 著者所属(英): The University of Tokyo
• 著者名: Ryosuke, Sato
• 著者名(英): Ryosuke, Sato
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: A refinement type system can be used as a basis of a fully automated verification tool of higher-order functional programs. Most of existing refinement type systems are, however, designed for call-by-value programs, which are unsound for call-by-name programs. In this paper, we introduce a refinement type system for a call-by-name functional language. The most important difference between call-by-value and call-by-name for constructing a refinement type system is whether a variable can be treated as a value or not. The soundness of a typical refinement type systems depends on this fact. On the other hand, in a call-by-name program, since a variable is bound to a term, we cannot treat a variable as a value. To overcome this problem, we track when the term bound to a variable will be evaluated. If we found that a variable is already evaluated in some context, we can treat the variable as a value at the context. We also introduce a type inference algorithm and report on a prototype implementation and preliminary experiments.; ------------------------------; 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.31(2023) (online); ------------------------------
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: A refinement type system can be used as a basis of a fully automated verification tool of higher-order functional programs. Most of existing refinement type systems are, however, designed for call-by-value programs, which are unsound for call-by-name programs. In this paper, we introduce a refinement type system for a call-by-name functional language. The most important difference between call-by-value and call-by-name for constructing a refinement type system is whether a variable can be treated as a value or not. The soundness of a typical refinement type systems depends on this fact. On the other hand, in a call-by-name program, since a variable is bound to a term, we cannot treat a variable as a value. To overcome this problem, we track when the term bound to a variable will be evaluated. If we found that a variable is already evaluated in some context, we can treat the variable as a value at the context. We also introduce a type inference algorithm and report on a prototype implementation and preliminary experiments.; ------------------------------; 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.31(2023) (online); ------------------------------
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 16, 号 3, 発行日 2023-08-28
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会