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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Unno, H., & Kobayashi, N. (2008). On-demand refinement of dependent types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4989 LNCS, pp. 81–96). https://doi.org/10.1007/978-3-540-78969-7_8
Mendeley helps you to discover research relevant for your work.