Dependent type inference with interpolants

10 years 2 months ago
Dependent type inference with interpolants
We propose a novel type inference algorithm for a dependentlytyped functional language. The novel features of our algorithm are: (i) it can iteratively refine dependent types with interpolants until the type inference succeeds or the program is found to be illtyped, and (ii) in the latter case, it can generate a kind of counterexample as an explanation of why the program is ill-typed. We have implemented a prototype type inference system and tested it for several programs. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Languages, Reliability, Verification Keywords Dependent Types, Type Inference
Hiroshi Unno, Naoki Kobayashi
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where PPDP
Authors Hiroshi Unno, Naoki Kobayashi
Comments (0)