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

• Type: Conference
• Year: 2009
• Where: PPDP
• Authors: Hiroshi Unno, Naoki Kobayashi
• Keywords: PPDP 2009, Programming Languages, Prototype Type Inference, Type Inference, Type Inference Algorithm