Extensions and Applications of Refinement Types based on Game Semantics

2015 Fiscal Year Final Research Report

• Project/Area Number: 25730035
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: University of Tsukuba
• Principal Investigator: Unno Hiroshi 筑波大学, システム情報系, 助教 (80569575)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: プログラム検証 / 型システム / 定理自動証明 / 制約解消

Outline of Final Research Achievements

The aim of this research project was to extend refinement type systems and their type checking and inference methods based on a denotational semantics, with applications to formal verification of high-level programs. The main result is the development of a fully-automated tool RCaml for path-sensitive verification of (a) termination, (b) non-termination, and (c) relational properties of high-order functional programs that manipulate algebraic data structures.

Free Research Field

情報科学