Termination checking with types

Andreas Abel

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2004)

  • Volume: 38, Issue: 4, page 277-319
  • ISSN: 0988-3754

Abstract

top
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Λ μ + , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

How to cite

top

Abel, Andreas. "Termination checking with types." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 38.4 (2004): 277-319. <http://eudml.org/doc/244766>.

@article{Abel2004,
abstract = {The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces $\Lambda _\mu ^+$, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.},
author = {Abel, Andreas},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {type-based termination; sized types; inductive types; course-of-value recursion; bidirectional type checking; strong normalization; Type-based termination},
language = {eng},
number = {4},
pages = {277-319},
publisher = {EDP-Sciences},
title = {Termination checking with types},
url = {http://eudml.org/doc/244766},
volume = {38},
year = {2004},
}

TY - JOUR
AU - Abel, Andreas
TI - Termination checking with types
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2004
PB - EDP-Sciences
VL - 38
IS - 4
SP - 277
EP - 319
AB - The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces $\Lambda _\mu ^+$, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.
LA - eng
KW - type-based termination; sized types; inductive types; course-of-value recursion; bidirectional type checking; strong normalization; Type-based termination
UR - http://eudml.org/doc/244766
ER -

References

top
  1. [1] A. Abel, Specification and verification of a formal system for structurally recursive functions, in Types for Proof and Programs, International Workshop, TYPES ’99, edited by T. Coquand, P. Dybjer, B. Nordström, J. Smith, Springer. Lect. Notes Comput. Sci. 1956 (2000) 1–20. Zbl0988.68054
  2. [2] A. Abel, A third-order representation of the λ μ -calculus, edited by S. Ambler, R. Crole, A. Momigliano, Elsevier Science Publishers. Electron. Notes Theor. Comput. Sci. 58 (2001). 
  3. [3] A. Abel, Termination and guardedness checking with continuous types, in Typed Lambda Calculi and Applications (TLCA 2003), edited by M. Hofmann, Valencia, Spain, Springer. Lect. Notes Comput. Sci. 2701 (2003) 1–15. Zbl1039.68029
  4. [4] A. Abel, Soundness of a bidirectional typing algorithm. Twelf code, available on the author’s homepage, http://www.tcs.informatik.uni-muenchen.de/ abel (May 2004). 
  5. [5] A. Abel and T. Altenkirch, A predicative analysis of structural recursion. J. Funct. Programming 12 (2002) 1–41. Zbl0998.68027
  6. [6] T. Altenkirch, Constructions, Inductive Types and Strong Normalization. Ph.D. Thesis, University of Edinburgh (Nov. 1993). 
  7. [7] R.M. Amadio and S. Coupet-Grimal, Analysis of a guard condition in type theory, in Foundations of Software Science and Computation Structures, First International Conference, FoSSaCS’98, edited by M. Nivat, Springer. Lect. Notes Comput. Sci. 1378 (1998). Zbl0922.03021
  8. [8] T. Arts and J. Giesl, Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236 (2000) 133–178. Zbl0938.68051
  9. [9] G. Barthe, M.J. Frade, E. Giménez, L. Pinto and T. Uustalu, Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14 (2004) 1–45. Zbl1054.68027
  10. [10] G.M. Bierman, A computational interpretation of the λ μ -calculus, in Proc. of Symposium on Mathematical Foundations of Computer Science, edited by L. Brim, J. Gruska, J. Zlatuska, Brno, Czech Republic. Lect. Notes Comput. Sci. 1450 (1998) 336–345. Zbl0912.03009
  11. [11] F. Blanqui, Type Theory and Rewriting. Ph.D. Thesis, Université Paris XI (Sept. 2001). 
  12. [12] F. Blanqui, A type-based termination criterion for dependently-typed higher-order rewrite systems, in 15th International Conference on Rewriting Techniques and Applications (RTA 04), June 3–5, 2004, Aachen, Germany, Springer. Lect. Notes Comput. Sci. 3091 (2004) 24–39. Zbl1187.68273
  13. [13] F. Blanqui, J.-P. Jouannaud and M. Okada, Inductive data type systems. Theor. Comput. Sci. 277 (2001). Zbl0992.68121MR1870362
  14. [14] J. Brauburger and J. Giesl, Termination analysis for partial functions, in Proc. of the Third International Static Analysis Symposium (SAS’96), Aachen, Germany, Springer. Lect. Notes Comput. Sci. 1145 (1996). Zbl0972.68031
  15. [15] W.-N. Chin and S.-C. Khoo, Calculating sized types. Higher-Order and Symbolic Computation 14 (2001) 261–300. Zbl0994.68015
  16. [16] C. Coquand, Agda. WWW page (2000) http://www.cs.chalmers.se/ catarina/agda/ 
  17. [17] T. Coquand, Infinite objects in type theory, in Types for Proofs and Programs (TYPES ’93), edited by H. Barendregt, T. Nipkow, Springer. Lect. Notes Comput. Sci. 806 (1993) 62–78. 
  18. [18] T. Coquand, An algorithm for type-checking dependent types, in Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction, July 17–21, 1995, Kloster Irsee, Germany, Elsevier Science. Sci. Comput. Programming 26 167–177 (1996). Zbl0853.68102
  19. [19] K. Crary and S. Weirich, Resource bound certification, in Proc. of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA (Jan. 2000) 184–198. Zbl1323.68368
  20. [20] R. Davies and F. Pfenning, Intersection types and computational effects, in Proc. of the International Conference on Functional Programming (ICFP 2000), Montreal, Canada (Sept. 2000) 198–208. Zbl1321.68147
  21. [21] J. Dunfield and F. Pfenning, Tridirectional typechecking, in 31st Annual Symposium on Principles of Programming Languages (POPL’04), edited by N.D. Jones and X. Leroy, Venice, Italy. ACM (Jan. 2004) 281–292. 
  22. [22] J. Giesl, Termination of nested and mutually recursive algorithms. J. Automat. Reason. 19 (1997) 1–29. Zbl0882.68019
  23. [23] E. Giménez, Structural recursive definitions in type theory, in Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13–17 1998, Proc., Springer. Lect. Notes Comput. Sci. 1443 (1998) 397–408. Zbl0910.03022
  24. [24] C. Haack and J.B. Wells, Type error slicing in implicitly typed, higher-order languages, in Programming Languages and Systems, 12th European Symp. Programming, Springer. Lect. Notes Comput. Sci. 2618 (2003) 284–301. Zbl1032.68041
  25. [25] T. Hagino, A typed lambda calculus with categorical type constructors, in Category Theory and Computer Science, edited by D.H. Pitt, A. Poigné, D.E. Rydeheard. Lect. Notes Comput. Sci. 283 (1987) 140–157. Zbl0643.03010
  26. [26] T. Hallgren, Alfa home page. http://www.math.chalmers.se/ hallgren/Alfa/ (2003). 
  27. [27] J. Hughes and L. Pareto, Recursion and dynamic data-structures in bounded space: Towards embedded ML programming, in International Conference on Functional Programming (ICFP’99) (1999) 70–81. 
  28. [28] J. Hughes, L. Pareto and A. Sabry, Proving the correctness of reactive systems using sized types, in Symposium on Principles of Programming Languages (1996) 410–423. 
  29. [29] INRIA, The Coq Proof Assistant Reference Manual, version 8.0 edition (April 2004). http://coq.inria.fr/doc/main.html 
  30. [30] C.S. Lee, N.D. Jones and A.M. Ben-Amram, The size-change principle for program termination, in ACM Symposium on Principles of Programming Languages (POPL’01), London, UK. ACM Press (Jan. 2001). Zbl1323.68216
  31. [31] Z. Luo, ECC: An Extended Calculus of Constructions. Ph.D. Thesis, University of Edinburgh (1990). Zbl0723.03034
  32. [32] R. Matthes, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. Thesis, Ludwig-Maximilians-University (May 1998). Zbl0943.68086
  33. [33] C. McBride, Dependently Typed Functional Programs and their Proofs. Ph.D. Thesis, University of Edinburgh (1999). 
  34. [34] N.P. Mendler, Recursive types and type constraints in second-order lambda calculus, in Proc. of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, New York. IEEE Computer Society Press (1987) 30–36. 
  35. [35] N.P. Mendler, Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Logic 51 (1991) 159–172. Zbl0719.03008
  36. [36] R. Milner, A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (1978) 348–375. Zbl0388.68003
  37. [37] L. Pareto, Types for Crash Prevention. Ph.D. Thesis, Chalmers University of Technology (2000). 
  38. [38] M. Parigot, λ μ -calculus: An algorithmic interpretation of classical natural deduction, in Logic Programming and Automated Reasoning: Proc. of the International Conference LPAR’92, edited by A. Voronkov, Springer, Berlin, Heidelberg (1992) 190–201. Zbl0925.03092
  39. [39] F. Pfenning and C. Schürmann, System description: Twelf – a meta-logical framework for deductive systems, in Proc. of the 16th International Conference on Automated Deduction (CADE-16), edited by H. Ganzinger, Springer, Trento, Italy. Lect. Notes Artif. Intell. 1632 (1999) 202–206. 
  40. [40] B. Pientka, Termination and reduction checking for higher-order logic programs, in Automated Reasoning, First International Joint Conference, IJCAR 2001, edited by R. Goré, A. Leitsch, and T. Nipkow, Springer. Lect. Notes Artif. Intell. 2083 (2001) 401–415. Zbl0988.68514
  41. [41] B.C. Pierce, Types and Programming Languages. MIT Press (2002). Zbl0995.68018MR1887075
  42. [42] B.C. Pierce, D.N. Turner, Local type inference, in POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California (1998). 
  43. [43] R. Pollack, The Theory of LEGO. Ph.D. Thesis, University of Edinburgh (1994). 
  44. [44] Z. Spławski and P. Urzyczyn, Type fixpoints: Iteration vs. recursion, in Proc. of the 1999 International Conference on Functional Programming (ICFP), Paris, France. SIGPLAN Notices 34 (1999) 102–113. 
  45. [45] A.J. Telford and D.A. Turner, Ensuring streams flow, in Algebraic Methodology and Software Technology (AMAST ’97), Springer. Lect. Notes Comput. Sci. 1349 (1997) 509–523. 
  46. [46] A.J. Telford and D.A. Turner, Ensuring termination in ESFP, in Proc. of BCTCS 15, 1999. J. Universal Comput. Sci. 6 (2000) 474–488. Zbl0960.68025
  47. [47] T. Uustalu and V. Vene, Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica (Lithuanian Academy of Sciences) 10 (1999) 5–26. Zbl0935.68011
  48. [48] C. Walther, Argument-Bounded Algorithms as a Basis for Automated Termination Proofs, in 9th International Conference on Automated Deduction, edited by E.L. Lusk and R.A. Overbeek, Springer. Lect. Notes Comput. Sci. 310 (1988) 602–621. Zbl0656.68104
  49. [49] A.K. Wright and M. Felleisen, A syntactic approach to type soundness. Inform. Comput. 115 (1994) 38–94. Zbl0938.68559
  50. [50] H. Xi, Dependent types for program termination verification. J. Higher-Order and Symbolic Computation 15 (2002) 91–131. Zbl1041.68059
  51. [51] J. Yang, G. Michaelson and P. Trinder, Explaining polymorphic types. Comput. J. 45 (2002) 436–452. Zbl1037.68019

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.