×

Termination checking with types. (English) Zbl 1089.68028

Summary: The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces \(\boldsymbol{\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.

MSC:

68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems

Software:

ML; LEGO; Twelf; Coq
PDFBibTeX XMLCite
Full Text: DOI Numdam EuDML Link

References:

[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 . Zbl 0988.68054 · Zbl 0988.68054
[2] A. Abel , A third-order representation of the \(\lambda \mu \)-calculus , edited by S. Ambler, R. Crole, A. Momigliano, Elsevier Science Publishers. Electron. Notes Theor. Comput. Sci. 58 ( 2001 ). · Zbl 1268.68045
[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 . Zbl 1039.68029 · Zbl 1039.68029
[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] A. Abel and T. Altenkirch , A predicative analysis of structural recursion . J. Funct. Programming 12 ( 2002 ) 1 - 41 . Zbl 0998.68027 · Zbl 0998.68027 · doi:10.1017/S0956796801004191
[6] T. Altenkirch , Constructions , Inductive Types and Strong Normalization. Ph.D. Thesis, University of Edinburgh (Nov. 1993).
[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 ). Zbl 0922.03021 · Zbl 0922.03021
[8] T. Arts and J. Giesl , Termination of term rewriting using dependency pairs . Theor. Comput. Sci. 236 ( 2000 ) 133 - 178 . Zbl 0938.68051 · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8
[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 . Zbl 1054.68027 · Zbl 1054.68027 · doi:10.1017/S0960129503004122
[10] G.M. Bierman , A computational interpretation of the \(\lambda \mu \)-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 . Zbl 0912.03009 · Zbl 0912.03009
[11] F. Blanqui , Type Theory and Rewriting . Ph.D. Thesis, Université Paris XI (Sept. 2001).
[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 . · Zbl 1187.68273
[13] F. Blanqui , J.-P. Jouannaud and M. Okada , Inductive data type systems . Theor. Comput. Sci. 277 ( 2001 ). MR 1870362 | Zbl 0992.68121 · Zbl 0992.68121 · doi:10.1016/S0304-3975(00)00347-9
[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 ).
[15] W.-N. Chin and S.-C. Khoo , Calculating sized types . Higher-Order and Symbolic Computation 14 ( 2001 ) 261 - 300 . Zbl 0994.68015 · Zbl 0994.68015 · doi:10.1023/A:1012996816178
[16] C. Coquand , Agda . WWW page ( 2000 ) http://www.cs.chalmers.se/ catarina/agda/ [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 .
[17] 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 ). Zbl 0853.68102 · Zbl 0853.68102 · doi:10.1016/0167-6423(95)00021-6
[18] 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 . · Zbl 1323.68368
[19] 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 . · Zbl 1321.68147
[20] 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 . · Zbl 1325.68062
[21] J. Giesl , Termination of nested and mutually recursive algorithms . J. Automat. Reason. 19 ( 1997 ) 1 - 29 . Zbl 0882.68019 · Zbl 0882.68019 · doi:10.1023/A:1005797629953
[22] 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 . Zbl 0910.03022 · Zbl 0910.03022
[23] 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 . Zbl 1032.68041 · Zbl 1032.68041
[24] 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 . Zbl 0643.03010 · Zbl 0643.03010
[25] T. Hallgren , Alfa home page . http://www.math.chalmers.se/ hallgren/Alfa/ ( 2003 ).
[26] 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 . · Zbl 1345.68061
[27] 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 .
[28] INRIA, The Coq Proof Assistant Reference Manual, version 8.0 edition (April 2004). http://coq.inria.fr/doc/main.html [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).
[29] Z. Luo , ECC: An Extended Calculus of Constructions . Ph.D. Thesis, University of Edinburgh ( 1990 ). Zbl 0723.03034 · Zbl 0723.03034
[30] R. Matthes , Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types . Ph.D. Thesis, Ludwig-Maximilians-University (May 1998). Zbl 0943.68086 · Zbl 0943.68086
[31] C. McBride , Dependently Typed Functional Programs and their Proofs . Ph.D. Thesis, University of Edinburgh ( 1999 ).
[32] 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 .
[33] N.P. Mendler , Inductive types and type constraints in the second-order lambda calculus . Ann. Pure Appl. Logic 51 ( 1991 ) 159 - 172 . Zbl 0719.03008 · Zbl 0719.03008 · doi:10.1016/0168-0072(91)90069-X
[34] R. Milner , A theory of type polymorphism in programming . J. Comput. Syst. Sci. 17 ( 1978 ) 348 - 375 . Zbl 0388.68003 · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[35] L. Pareto , Types for Crash Prevention . Ph.D. Thesis, Chalmers University of Technology ( 2000 ).
[36] M. Parigot , \(\lambda \mu \)-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 . Zbl 0925.03092 · Zbl 0925.03092
[37] 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 .
[38] 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 . Zbl 0988.68514 · Zbl 0988.68514
[39] B.C. Pierce , Types and Programming Languages . MIT Press ( 2002 ). MR 1887075 | Zbl 0995.68018 · Zbl 0995.68018
[40] 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 ).
[41] R. Pollack , The Theory of LEGO . Ph.D. Thesis, University of Edinburgh ( 1994 ).
[42] 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 . · Zbl 1343.03010
[43] 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 .
[44] 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 . Zbl 0960.68025 · Zbl 0960.68025
[45] T. Uustalu and V. Vene , Primitive (co)recursion and course-of-value (co)iteration, categorically . Informatica (Lithuanian Academy of Sciences) 10 ( 1999 ) 5 - 26 . Zbl 0935.68011 · Zbl 0935.68011
[46] 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 . Zbl 0656.68104 · Zbl 0656.68104
[47] A.K. Wright and M. Felleisen , A syntactic approach to type soundness . Inform. Comput. 115 ( 1994 ) 38 - 94 . Zbl 0938.68559 · Zbl 0938.68559 · doi:10.1006/inco.1994.1093
[48] H. Xi , Dependent types for program termination verification . J. Higher-Order and Symbolic Computation 15 ( 2002 ) 91 - 131 . Zbl 1041.68059 · Zbl 1041.68059 · doi:10.1023/A:1019916231463
[49] J. Yang , G. Michaelson and P. Trinder , Explaining polymorphic types . Comput. J. 45 ( 2002 ) 436 - 452 . Zbl 1037.68019 · Zbl 1037.68019 · doi:10.1093/comjnl/45.4.436
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.