Sciweavers

Share
FLOPS
2008
Springer

On-Demand Refinement of Dependent Types

9 years 11 months ago
On-Demand Refinement of Dependent Types
Dependent types are useful for statically checking detailed specifications of programs and detecting pattern match or array bounds errors. We propose a novel approach to applications of dependent types to practical programming languages: Instead of requiring programmers' declaration of dependent function types (as in Dependent ML) or trying to infer them from function definitions only (as in size inference), we mine the output specification of a dependent function from the function's call sites, and then propagate that specification backward to infer the input specification. We have implemented a prototype type inference system which supports higher-order functions, parametric polymorphism, and algebraic data types based on our approach, and obtained promising experimental results.
Hiroshi Unno, Naoki Kobayashi
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FLOPS
Authors Hiroshi Unno, Naoki Kobayashi
Comments (0)
books