Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL 1996, pp. 410–423. ACM Press, New York (1996)
Chin, W.N., Khoo, S.C.: Calculating sized types. In: PEPM 2000, pp. 62–72. ACM Press, New York (1999)
Chin, W.N., Khoo, S.C., Xu, D.N.: Extending sized type with collection analysis. In: PEPM 2003, pp. 75–84. ACM Press, New York (2003)
Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI 1998, pp. 249–257. ACM Press, New York (1998)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL 1999, pp. 214–227. ACM Press, New York (1999)
Knowles, K., Flanagan, C.: Type Reconstruction for General Refinement Types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 505–519. Springer, Heidelberg (2007)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001, pp. 203–213. ACM Press, New York (2001)
Unno, H., Kobayashi, N.: On-demand refinement of dependent types (Full version) (January, 2008), http://web.yl.is.s.u-tokyo.ac.jp/~uhiro/
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84–96. ACM Press, New York (1978)
Popeea, C., Chin, W.N.: Inferring disjunctive postconditions. In: ASIAN 2006. LNCS, Springer, Heidelberg (December, 2006)
Dunfield, J.: Combining two forms of type refinements. Technical Report CMU-CS-02-182, Carnegie Mellon University (September, 2002)
Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: POPL 2004, pp. 281–292. ACM Press, New York (2004)
Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL 2003, pp. 224–235. ACM Press, New York (2003)
Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic data types. In: POPL 2006, pp. 232–244. ACM Press, New York (2006)
Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP 2006, pp. 50–61. ACM Press, New York (2006)
Sulzmann, M., Voicu, R.: Language-based program verification via expressive types. Electronic Notes in Theoretical Computer Science 174(7), 129–147 (2007)
Kiselyov, O., Shan, C.c.: Lightweight static capabilities. Electronic Notes in Theoretical Computer Science 174(7), 79–104 (2007)
Pierce, B.C., Turner, D.N.: Local type inference. In: POPL 1998, pp. 252–265. ACM Press, New York (1998)
Flanagan, C.: Hybrid type checking. In: POPL 2006, pp. 245–256. ACM Press, New York (2006)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42–54. ACM Press, New York (2006)
Chlipala, A.: Modular development of certified program verifiers with a proof assistant. In: ICFP 2006, pp. 160–171. ACM Press, New York (2006)
Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter. Manuscript (April, 2005)
Augustsson, L.: Cayenne – a language with dependent types. In: ICFP 1998: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pp. 239–250. ACM Press, New York (1998)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL 2002, pp. 191–202. ACM Press, New York (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58–70. ACM Press, New York (2002)
Suzuki, N., Ishihata, K.: Implementation of an array bound checker. In: POPL 1977, pp. 132–143. ACM Press, New York (1977)
Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53–68. Springer, Heidelberg (2004)
Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI 2007, pp. 300–309. ACM Press, New York (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Unno, H., Kobayashi, N. (2008). On-Demand Refinement of Dependent Types. In: Garrigue, J., Hermenegildo, M.V. (eds) Functional and Logic Programming. FLOPS 2008. Lecture Notes in Computer Science, vol 4989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78969-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-78969-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78968-0
Online ISBN: 978-3-540-78969-7
eBook Packages: Computer ScienceComputer Science (R0)