Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Dependent Types for Program Termination Verification

  • Published:
Higher-Order and Symbolic Computation

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, and polymorphism.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abel, A. and Altenkirch, T. A predicative strong normalisation proof for a λ-calculus with interleaving inductive types. In Proceedings of International Workshop on Types for Proof and Programs (TYPES '99), T. Coquand, P. Dybjer, B. Nordström, and J. Smith (Eds.). LNCS,Vol. 1956, Springer-Verlag, 2000, pp. 21–40.

  2. BenCherifa, A. and Lescanne, P. Termination of rewriting systems by polynomial interpretations and its implementation. SCP, 9(2) (1987) 137–160.

    Google Scholar 

  3. Chang, C.C. and Keisler, H.J. Model Theory, Studies in Logic and Mathematical Foundations, Vol. 73. North-Holland, Amsterdam, The Netherlands, 1977.

    Google Scholar 

  4. Chin, W.-N. and Khoo, S.-C. Calculating sized types. Higher-Order and Symbolic Computation, 14(2/3), to appear.

  5. Constable, R.L. et al. Implementing Mathematics with the NuPrl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

    Google Scholar 

  6. Crary, K. and Weirich, S. Resource bound certification. In Proceedings of 27th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2000), Boston, 2000, pp. 184–198.

  7. Dershowitz, N. Orderings for term rewriting systems. Theoretical Computer Science, 17(3) (1982) 279–301.

    Google Scholar 

  8. Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., and Werner, B. The Coq proof assistant user's guide. Rapport Technique 154, INRIA, Rocquencourt, France. Version 5.8. 1993.

    Google Scholar 

  9. Girard, J.-Y. Interprétation Fonctionnelle et Élimination des Coupures dans l'Arithmétique d'Ordre Supérieur. Thèse de doctorat d'état, Université de Paris VII, Paris, France, 1972.

    Google Scholar 

  10. Girard, J.-Y., Lafont, Y., and Taylor, P. Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Vol. 7, Cambridge University Press, Cambridge, England, 1989.

    Google Scholar 

  11. Grobauer, B. Cost recurrences for DML programs. In Proceedings of Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01), Florence, Italy, 2001, pp. 253–264.

  12. Harper, R. Proof-directed debugging. Journal of Functional Programming, 9(4) (1999) 471–477.

    Google Scholar 

  13. Hughes, J., Pareto, L., and Sabry, A. Proving the correctness of reactive systems using sized types. In Conference Record of 23rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '96), 1996, pp. 410–423.

  14. Jouannaud, J.-P. and Rubio, A. The higher-order recursive path ordering. In Proceedings of 14th IEEE Symposium on Logic in Computer Science (LICS '99), Trento, Italy, 1999, pp. 402–411.

  15. Lee, C.S., Jones, N.D., and Ben-Amram, A.M. The size-change principle for program termination. In Proceeding of the 28th ACM Symposium on Principles of Programming Languages (POPL '01), London, UK, 2001, pp. 81–92.

  16. Milner, R., Tofte, M., Harper, R.W., and MacQueen, D. The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts, 1997.

    Google Scholar 

  17. Necula, G. Proof-carrying code. In Conference Record of 24th Annual ACM Symposium on Principles of Programming Languages, ACM Press, Paris, France, 1997, pp. 106–119.

    Google Scholar 

  18. Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. PVS: Combining specification, proof checking, and model checking. In Proceedings of the 8th International Conference on Computer-Aided Verification (CAV '96), R. Alur and T.A. Henzinger (Eds.). New Brunswick, NJ, LNCS, Vol. 1102, Springer-Verlag, 1996, pp. 411–414.

    Google Scholar 

  19. Paulson, L. Isabelle: A Generic Theorem Prover. LNCS, Vol. 828, Springer-Verlag, 1994.

  20. Pientka, B. and Pfenning, F. Termination and reduction checking in the logical framework. In Proceedings of Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, PA, 2000.

  21. Speirs, C., Somogyi, Z., and Søndergaard, H. Termination Analysis for Mercury. In Proceedings of the 4th Static Analysis Symposium (SAS '97), P.V. Hentenryck (Ed.). Paris, France, LNCS,Vol. 1302, Springer-Verlag, 1997, pp. 157–171.

    Google Scholar 

  22. Tait, W.W. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2) (1967) 198–212.

    Google Scholar 

  23. Ullman, J.D. and Van Gelder, A. Efficient tests for top-down termination of logic rules. Journal of the ACM, 35(2) (1988) 345–373.

    Google Scholar 

  24. Xi, H. Dependent types in practical programming. Ph.D. Thesis, Carnegie Mellon University, 1998, pp. viii+189. Available as http://www.cs.cmu.edu/~hwxi/DML/thesis.ps.

  25. Xi, H. Dependent ML, 1999. Available at http://www.cs.bu.edu/~hwxi/DML/DML.html.

  26. Xi, H. Dependently typed data structures. In Proceedings of Workshop on Algorithmic Aspects of Advanced Programming Languages, Paris, France, 1999, pp. 17–33.

  27. Xi, H. Dependent types for program termination verification, 2000. Available as http://www.cs.bu.edu/~hwxi/DML/Term.

  28. Xi, H. and Pfenning, F. Eliminating array bound checking through dependent types. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Montréal, Canada, 1998, pp. 249–257.

  29. Xi, H. and Pfenning, F. Dependent types in practical programming. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, 1999, pp. 214–227.

  30. Zantema, H. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24 (1995) 89–105.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Boston University, Boston, MA, 02215, USA

    Hongwei Xi

Authors
  1. Hongwei Xi
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Xi, H. Dependent Types for Program Termination Verification. Higher-Order and Symbolic Computation 15, 91–131 (2002). https://doi.org/10.1023/A:1019916231463

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1019916231463

Search

Navigation