Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-24T22:37:43.010Z Has data issue: false hasContentIssue false
  • English
  • Français

Size-based termination of higher-order rewriting

Published online by Cambridge University Press:  19 April 2018

FRÉDÉRIC BLANQUI
FRÉDÉRIC BLANQUI*
Affiliation:
INRIA, ENS / Université Paris-Saclay, LSV, 61 avenue du Président Wilson, 94235 Cachan Cedex, France (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We provide a general and modular criterion for the termination of simply typed λ-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.

Type
Research Article
Information
Journal of Functional Programming , Volume 28 , 2018 , e11
Copyright
Copyright © Cambridge University Press 2018 

References

Abel, A. (2004) Termination checking with types. Theor. Inform. Appl. 38 (4), 277–319.Google Scholar
Abel, A. (2006) A Polymorphic Lambda-Calculus with Sized Higher-Order Types, Ph.D. thesis. Germany: Ludwig-Maximilians-Universität München.Google Scholar
Abel, A. (2008) Semi-continuous sized types and termination. Log. Methods Comput. Sci. 4 (2), 1–33.Google Scholar
Abel, A. (2010) MiniAgda: Integrating sized and dependent types. In Proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers, Electronic Proceedings in Theoretical Computer Science, vol. 43.Google Scholar
Abel, A. (2012) Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In Proceedings of the 8th Workshop on Fixed-points in Computer Science, Electronic Proceedings in Theoretical Computer Science, vol. 77.CrossRefGoogle Scholar
Abel, A. & Altenkirch, T. (2002) A predicative analysis of structural recursion. J. Funct. Program. 12 (1), 1–41.Google Scholar
Ackermann, W. (1925) Begründung des "tertium non datur" mittels der Hilbertschen Theorie der Widerspruchsfreiheit. Math. Ann. 93, 1–36.Google Scholar
Agda. (2017) Accessed March 8, 2018. Available at: http://wiki.portal.chalmers.se/agda/pmwiki.php.Google Scholar
Amadio, R. & Coupet-Grimal, S. (1997) Analysis of a Guard Condition in Type Theory (preliminary report). Technical Report 3300. France: INRIA.Google Scholar
Amadio, R. & Coupet-Grimal, S. (1998) Analysis of a guard condition in type theory (Extended abstract). In Proceedings of the 1st International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 1378.Google Scholar
Arts, T. (1996) Termination by absence of infinite chains of dependency pairs. In Proceedings of the 21st Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science, vol. 1059.Google Scholar
Arts, T. & Giesl, J. (2000) Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133–178.Google Scholar
ATS. (2018) Accessed March 8, 2018. Available at: http://www.ats-lang.org/.Google Scholar
Avanzini, M. & Moser, G. (2010) Closing the gap between runtime complexity and polytime computability. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics, vol. 6.Google Scholar
Baccelli, F., Cohen, G., Olsder, G. J. & Quadrat, J.-P. (1992) Synchronization and Linearity: An Algebra for Discrete Event Systems. Wiley.Google Scholar
Barbanera, F., Fernández, M. & Geuvers, H. (1997) Modularity of strong normalization in the algebraic-λ-cube. J. Funct. Program. 7 (6), 613–660.Google Scholar
Barthe, G., Frade, M. J., Giménez, E., Pinto, L. & Uustalu, T. (2004) Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14 (1), 97–141.Google Scholar
Barthe, G., Grégoire, B. & Pastawski, F. (2005) Practical inference for type-based termination in a polymorphic setting. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 3461.Google Scholar
Barthe, G., Grégoire, B. & Pastawski, F. (2006) CIC$\widehat{~}$: Type-based termination of recursive definitions in the calculus of inductive constructions. In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science, vol. 4246.Google Scholar
Barthe, G., Grégoire, B. & Riba, C. (2008) Type-based termination with sized products. In Proceedings of the 22nd International Conference on Computer Science Logic, Lecture Notes in Computer Science, vol. 5213.Google Scholar
Ben-Amram, A. M. & Codish, M. (2008) A SAT-based approach to size change termination with global ranking functions. In Proceedings of the 14th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 4963.Google Scholar
Berger, U. (2005) Continuous semantics for strong normalization. In Proceedings of the 1st Conference on Computability in Europe, Lecture Notes in Computer Science, vol. 3526.Google Scholar
Berger, U. (2008) A domain model characterising strong normalisation. Ann. Pure Appl. Log. 156 (1), 39–50.Google Scholar
Blanqui, F. (2000) Termination and confluence of higher-order rewrite systems. In Proceedings of the 11th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1833.Google Scholar
Blanqui, F. (2004) A type-based termination criterion for dependently-typed higher-order rewrite systems. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 3091.Google Scholar
Blanqui, F. (2005a) Decidability of type-checking in the calculus of algebraic constructions with size annotations. In Proceedings of the 19th International Conference on Computer Science Logic, Lecture Notes in Computer Science, vol. 3634.Google Scholar
Blanqui, F. (2005b) Definitions by rewriting in the calculus of constructions. Math. Struct. Comput. Sci. 15 (1), 37–92.Google Scholar
Blanqui, F. (2006a) Higher-order dependency pairs. In Proceedings of the 8th International Workshop on Termination.Google Scholar
Blanqui, F. (2006b) (HO)RPO Revisited. Technical Report 5972. France: INRIA.Google Scholar
Blanqui, F. (2016) Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. Theor. Comput. Sci. 611, 50–86.Google Scholar
Blanqui, F. & Riba, C. (2006) Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science, vol. 4246.Google Scholar
Blanqui, F. & Roux, C. (2009) On the relation between sized-types based termination and semantic labelling. In Proceedings of the 23rd International Conference on Computer Science Logic, Lecture Notes in Computer Science, vol. 5771.CrossRefGoogle Scholar
Blanqui, F., Jouannaud, J.-P. & Okada, M. (2002) Inductive-data-type systems. Theor. Comput. Sci. 272, 41–68.Google Scholar
Blanqui, F., Jouannaud, J.-P. & Rubio, A. (2015) The computability path ordering. Log. Methods Comput. Sci. 11 (4), 1–45.Google Scholar
Bonfante, G., Marion, J.-Y. & Péchoux, R. (2011) Quasi-interpretations a way to control resources. Theor. Comput. Sci. 412 (25), 2776–2796.CrossRefGoogle Scholar
Borralleras, C. & Rubio, A. (2001) A monotonic higher-order semantic path ordering. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science, vol. 2250.Google Scholar
Boyer, R. & Moore, J. (1979) A Computational Logic. Academic Press.Google Scholar
Breazu-Tannen, V. & Gallier, J. (1989) Polymorphic rewriting conserves algebraic strong normalization. In Proceedings of the 16th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 372.Google Scholar
Burstall, R., Queen, D. Mac & Sannella, D. (1980) HOPE: An experimental applicative language. In Proceedings of the ACM Symposium on Lisp and Fonctional Programming.Google Scholar
Cheney, J. (2003) First-Class Phantom Types. Technical Report TR2003-1901. Cornell University.Google Scholar
Cherifa, A. B. & Lescanne, P. (1987) Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program. 9 (2), 137–159.Google Scholar
Chin, W. N. & Khoo, S. C. (2001) Calculating sized types. J. Higher-Order Symb. Comput. 14 (2–3), 261–300.Google Scholar
Church, A. (1940) A formulation of the simple theory of types. J. Symb. Log. 5, 56–68.CrossRefGoogle Scholar
Cichoń, E. A. & Touzet, H. (1996) An ordinal calculus for proving termination in term rewriting. In Proceedings of the 21st Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science, vol. 1059.Google Scholar
cicminus. (2015) Accessed March 8, 2018. Available at: https://github.com/jsacchini/coq.Google Scholar
Codish, M., Giesl, J., Schneider-Kamp, P. & Thiemann, R. (2011) SAT solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reason. 49 (1), 53–93.Google Scholar
Collins, G. (1975) Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33.Google Scholar
Contejean, E., Marché, C., Tomás, A. P. & Urbain, X. (2005) Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34 (4), 325–363.Google Scholar
Coq. (2017) Accessed March 8, 2018. Available at: http://coq.inria.fr/.Google Scholar
Coquand, T. & Paulin-Mohring, C. (1988) Inductively defined types. In Proceedings of the International Conference on Computer Logic, Lecture Notes in Computer Science, vol. 417.Google Scholar
Coquand, T. & Spiwack, A. (2007) A proof of strong normalization using domain theory. Log. Methods Comput. Sci. 3 (4), 1–16.Google Scholar
Courtieu, P., Gbedo, G. & Pons, O. (2010) Improved matrix interpretation. In Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science, Lecture Notes in Computer Science, vol. 5901.Google Scholar
Cousot, P. (1996) Abstract interpretation. ACM Comput. Surv. 28 (2), 324–328.Google Scholar
Cousot, P. (1997) Types as abstract interpretations (invited paper). In Proceedings of the 24th ACM Symposium on Principles of Programming Languages.Google Scholar
Cousot, P. & Cousot, R. (1979) Constructive versions of Tarski's fixed point theorems. Pac. J. Math. 82 (1), 43–57.Google Scholar
Cuninghame-Green, R. (1979) Minimax Algebra. Lecture Notes in Economics and Mathematical Systems, no. 166. SV.Google Scholar
Curien, P.-L. & Ghelli, G. (1992) Coherence of subsumption, minimum typing and type-checking in F⩽. Log. Methods Comput. Sci. 2 (1), 55–91.Google Scholar
Curry, H. B. & Feys, R. (1958) Combinatory Logic. North-Holland, ISBN 9780444533876.Google Scholar
de Bruijn, N. G. (1970) The mathematical language AUTOMATH, its usage, and some of its extensions. In Proceedings of the 1968 Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol. 125.Google Scholar
de Vrijer, R. (1987) Exactly estimating functionals and strong normalization. Indagationes Math. 90 (4), 479–493.Google Scholar
Dedukti. (2018) Accessed March 8, 2018. Available at: https://deducteam.github.io/.Google Scholar
Dershowitz, N. (1979a) A note on simplification orderings. Inform. Process. Lett. 9 (5), 212–215.Google Scholar
Dershowitz, N. (1979b) Orderings for term rewriting systems. In Proceedings of the 20th IEEE Symposium on Foundations of Computer Science.Google Scholar
Dershowitz, N. (1982) Orderings for term rewriting systems. Theor. Comput. Sci. 17, 279–301.Google Scholar
Dershowitz, N. (2013) Dependency pairs are a simple semantic path ordering. In Proceedings of the 13th International Workshop on Termination.Google Scholar
Dershowitz, N. & Jouannaud, J.-P. (1990) Rewrite systems. In Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics, van Leeuwen, J. (ed), Chap. 6, pp. 243–320. North-Holland, ISBN 9780262220392.Google Scholar
Dershowitz, N. & Manna, Z. (1979) Proving termination with multiset orderings. Commun. ACM 22 (8), 465–476.Google Scholar
Dershowitz, N. & Okada, M. (1988) Proof-theoretic techniques for term rewriting. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science.Google Scholar
Endrullis, J., Waldmann, J. & Zantema, H. (2008) Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40 (2–3), 195–220.Google Scholar
Fiore, M., Plotkin, G. & Turi, D. (1999) Abstract syntax and variable binding. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science.Google Scholar
Fischer, M. & Rabin, M. (1974) Super-exponential complexity of Presburger arithmetic. In Proceedings of the SIAM-AMS Symposium in Applied Mathematics.Google Scholar
Fuh, Y.-C. & Mishra, P. (1990) Type inference with subtypes. Theor. Comput. Sci. 73 (2), 155–175.Google Scholar
Fuhs, C. & Kop, C. (2012) Polynomial interpretations for higher-order rewriting. In Proceedings of the 23rd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics, vol. 15.Google Scholar
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R. & Zankl, H. (2007) SAT solving for termination analysis with polynomial interpretations. In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol. 4501.CrossRefGoogle Scholar
Fuhs, C., Navarro, R., Otto, C., Giesl, J., Lucas, S. & Schneider-Kamp, P. (2008) Search techniques for rational polynomial orders. In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation, Lecture Notes in Computer Science, vol. 5144.Google Scholar
Gandy, R. O. (1980a) An early proof of normalization by A. M. Turing. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Hindley, R. & Seldin, J. P. (eds), Academic Press, pp. 453–455.Google Scholar
Gandy, R. O. (1980b) Proofs of strong normalization. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Hindley, R. & Seldin, J. P. (eds), Academic Press, pp. 457–477.Google Scholar
Gentzen, G. (1935) Die Widerspruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112 (1), 493–565. English translation in Szabo (1969).Google Scholar
Giesl, J. (1997) Termination of nested and mutually recursive algorithms. J. automated reason. 19 (1), 1–29.Google Scholar
Giesl, J., Arts, T. & Ohlebusch, E. (2002) Modular termination proofs for rewriting using dependency pairs. J. Symp. Comput. 34 (1), 21–58.Google Scholar
Giesl, J., Thiemann, R., Schneider-Kamp, P. & Falke, S. (2006) Mechanizing and improving dependency pairs. J. Autom. Reason. 37 (3), 155–203.Google Scholar
Giménez, E. (1996) Un calcul de constructions infinies et son application à la vérification de systèmes communiquants, PhD Thesis. France: ENS Lyon.Google Scholar
Giménez, E. (1998) Structural recursive definitions in type theory. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 1443.Google Scholar
Girard, J.-Y. (1972) Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur, PhD Thesis. France: Université Paris 7.Google Scholar
Girard, J.-Y., Lafont, Y. & Taylor, P. (1988) Proofs and Types. Cambridge University Press.Google Scholar
Gödel, K. (1931) Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Math. Phys. 38, 173–198. English translation in v. Heijenoort (1977).Google Scholar
Gödel, K. (1958) Über einer bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12 (3–4), 280–287. Reprinted in Gödel (1990).Google Scholar
Gödel, K. (1990) Collected works – vol. 2: publications 1938–1974. Oxford University Press.Google Scholar
Grégoire, B. & Sacchini, J. L. (2010) On strong normalization of the calculus of constructions with type-based termination. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science, vol. 6397.Google Scholar
Hamana, M. (2006) An initial algebra approach to term rewriting systems with variable binders. J. Higher-Order Symbol. Comput. 19 (2–3), 231–262.Google Scholar
Hamana, M. (2007) Higher-order semantic labelling for inductive datatype systems. In Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming.CrossRefGoogle Scholar
Hardy, G. H. (1904) A theorem concerning the infinite cardinal numbers. Q. J. Math. 35, 87–94.Google Scholar
Hartogs, F. (1915) Über das Problem der Wohlordnung. Math. Ann. 76, 438–443.CrossRefGoogle Scholar
Haskell. (2017) Accessed March 8, 2018. Available at: https://www.haskell.org/.Google Scholar
Herbrand, J. (1930) Recherches sur la théorie de la démonstration, Ph.D. thesis. France: Faculté des sciences de Paris.Google Scholar
Hessenberg, G. (1909) Kettentheorie und Wohlordnung. J. für die reine und angewandte Math. 135, 81–133.Google Scholar
Hindley, R. (1969) The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29–60.Google Scholar
Hirokawa, N. & Middeldorp, A. (2005) Automating the dependency pair method. Inform. Comput. 199 (1–2), 172–199.Google Scholar
Hirokawa, N. & Middeldorp, A. (2006) Predictive labeling. In Proceedings of the 17th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 4098.Google Scholar
Hofbauer, D. & Lautemann, C. (1989) Termination proofs and the length of derivations. In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 355.Google Scholar
Hong, H. & Jakuš, D. (1998) Testing positiveness of polynomials. J. Autom. Reason. 21 (1), 23–38.Google Scholar
HOT. (2012) Accessed March 8, 2018. Available at: http://rewriting.gforge.inria.fr/hot.html.Google Scholar
Howard, W. A. (1970) Assignment of ordinals to terms for primitive recursive functionals of finite type. In Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N. Y. Studies in Logic and the Foundations of Mathematics, vol. 60.Google Scholar
Howard, W. A. (1972) A system of abstract constructive ordinals. J. Symb. Log. 37 (2), 355–374.Google Scholar
Hrbacek, K. & Jech, T. (1999) Introduction to Set Theory. 3rd, revised and expanded edn. Dekker, M., Monographs and Texbooks in Pure and Applied Mathematics. Vol. 220. ISBN 9780824779153.Google Scholar
Huet, G. (1976) Résolution d'équations dans les langages d'ordre 1, 2, . . ., ω, Thèse d'État. France: Université Paris 7.Google Scholar
Huet, G. & Hullot, J.-M. (1982) Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci. 25 (2), 239–266.Google Scholar
Hughes, J., Pareto, L. & Sabry, A. (1996) Proving the correctness of reactive systems using sized types. In Proceedings of the 23th ACM Symposium on Principles of Programming Languages.Google Scholar
Hyvernat, P. (2014) The size-change termination principle for constructor based languages. Log. Methods Comput. Sci. 10 (1), 1–30.Google Scholar
Jones, N. D. & Bohr, N. (2008) Call-by-value termination in the untyped λ-calculus. Log. Methods Comput. Sci. 4 (1), 1–39.Google Scholar
Jouannaud, J.-P. & Okada, M. (1991) A computation model for executable higher-order algebraic specification languages. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science.Google Scholar
Jouannaud, J.-P. & Rubio, A. (1999) The higher-order recursive path ordering. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science.Google Scholar
Jouannaud, J.-P. & Rubio, A. (2007) Polymorphic higher-order recursive path orderings. J. ACM 54 (1), 1–48.Google Scholar
Kahrs, S. (1995) Towards a domain theory for termination proofs. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 914.Google Scholar
Kamin, S. & Lévy, J.-J. (1980) Available on http://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/KAMIN_LEVY/kamin-levy80spo.pdf. Attempts for generalizing the recursive path orderings. Unpublished note.Google Scholar
Klop, J. W., van Oostrom, V. & van Raamsdonk, F. (1993) Combinatory reduction systems: introduction and survey. Theor. Comput. Sci. 121, 279–308.Google Scholar
Knaster, B. & Tarski, A. (1928) Un théorème sur les fonctions d'ensembles. Ann. de la société polonaise de Math. 6, 133–134.Google Scholar
Kop, C. (2011) Higher order dependency pairs for algebraic functional systems. In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics, vol. 10.Google Scholar
Koprowski, A. & Zantema, H. (2006) Automation of recursive path ordering for infinite labelled rewrite systems. In Proceedings of the 3rd International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, vol. 4130.Google Scholar
Kuratowski, C. (1922) Une méthode d'élimination des nombres transfinis des raisonnements mathématiques. Fundam. Math. 3 (1), 76–108.Google Scholar
Kusakari, K., Isogai, Y., Sakai, M. & Blanqui, F. (2009) Static dependency pair method based on strong computability for higher-order rewrite systems. Ieice Trans. Inform. Syst. E92–D (10), 2007–2015.Google Scholar
Kusakari, K. & Sakai, M. (2007) Enhancing dependency pair method using strong computability in simply-typed term rewriting systems. Appl. Algebra Eng. Commun. Comput. 18 (5), 407–431.Google Scholar
Lee, C. S., Jones, N. D. & Ben-Amram, A. M. (2001) The size-change principle for program termination. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages.Google Scholar
Lucas, S. (2005) Polynomials over the reals in proofs of termination: from theory to practice. Theor. Inform. Appl. 39, 547–586.Google Scholar
Manna, Z. & Ness, S. (1970) On the termination of Markov algorithms. In Proceedings of the 3rd Hawaii International Conference on System Sciences.Google Scholar
Martin-Löf, P. (1975) An intuitionistic theory of types: predicative part. In Proceedings of the 1973 Logic Colloquium, Rose, H. E. & Shepherdson, J. C. (eds), Studies in Logic and the Foundations of Mathematics, vol. 80. North-Holland, ISBN 978044410642.Google Scholar
Matiyasevich, Y. V. (1970) Enumerable sets are diophantine. Sov. Math. Dokl. 11, 354–358.Google Scholar
Matiyasevich, Y. V. (1993) Hilbert's Tenth Problem. MIT Press.Google Scholar
Maude. (2015) Accessed March 8, 2018. Available at: http://maude.cs.uiuc.edu/.Google Scholar
Mayr, R. & Nipkow, T. (1998) Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192 (2), 3–29.Google Scholar
Mendler, N. P. (1987) Inductive Definition in Type Theory, Ph.D. Thesis. USA: Cornell University.Google Scholar
Mendler, N. P. (1991) Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Log. 51 (1–2), 159–172.Google Scholar
Middeldorp, A., Ohsaki, H. & Zantema, H. (1996) Transforming termination by self-labelling. In Proceedings of the 13th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 1104.CrossRefGoogle Scholar
Miller, D. (1991) A logic programming language with lambda-abstraction, function variables, and simple unification. In Proceedings of the International Workshop on Extensions of Logic Programming, Lecture Notes in Computer Science, vol. 475.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (3), 348–37s5.Google Scholar
MiniAgda. (2014) Accessed March 8, 2018. Available at: http://www.cse.chalmers.se/~abela/miniagda/index.html.Google Scholar
Mitchell, J. (1984) Coercion and type inference (summary). In Proceedings of the 11th ACM Symposium on Principles of Programming Languages.Google Scholar
Monin, F. & Simonot, M. (2001) An ordinal measure based procedure for termination of functions. Theor. Comput. Sci. 254 (1–2), 63–94.Google Scholar
Moser, G. (2017) KBOs, ordinals, subrecursive hierarchies and all that. J. Log. Comput. 27 (2), 1–27.Google Scholar
Newman, M. (1942) On theories with a combinatorial definition of "equivalence". Ann. Math. 43 (2), 223–243.Google Scholar
Nipkow, T. (1991) Higher-order critical pairs. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science.Google Scholar
OCaml. (2017) Accessed March 8, 2018. Available at: http://ocaml.org/.Google Scholar
Okada, M. (1989) Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In Proceedings of the International Symposium on Symbolic and Algebraic Computation.Google Scholar
Pareto, L. (2000) Types for Crash Prevention, PhD Thesis. Göteborg, Sweden: Chalmers University of Technology.Google Scholar
Paulson, L. (1986) Proving termination of normalization functions for conditional expressions. J. Autom. Reason. 2 (1), 63–74.Google Scholar
Peano, G. (1889) Arithmetices principia, nova methodo exposita. Fratres Bocca. Partial English translation in v. Heijenoort (1977).Google Scholar
Plotkin, G. D. (1977) LCF considered as a programming language. Theorm. Comput. Sci. 5 (3), 223–255.Google Scholar
Pottier, F. (2001) Simplifying subtyping constraints: A theory. Inform. Comput. 170 (2), 153–183.Google Scholar
Pratt, V. (1977) Available on http://boole.stanford.edu/pub/sefnp.pdf. Two Easy Theories Whose Combination is Hard. Unpublished note.Google Scholar
Presburger, M. (1929) Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Sprawozdanie z I Kongresu Matematykow Krajow Slowcanskich, Warszawa, Poland.Google Scholar
Rathjen, M. (2006) The art of ordinal analysis. In Proceedings of the International Congress of Mathematicians, vol. 2, pp. 45–69.Google Scholar
Riba, C. (2007) On the stability by union of reducibility candidates. In Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 4423.Google Scholar
Riba, C. (2008) Stability by union of reducibility candidates for orthogonal constructor rewriting. In Proceedings of the 4th Conference on Computability in Europe, Lecture Notes in Computer Science, vol. 5028.Google Scholar
Riba, C. (2009) On the values of reducibility candidates. In Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 5608.Google Scholar
Robinson, J. A. (1965) A machine-oriented logic based on the resolution principle. J. ACM 12 (1), 23–41.Google Scholar
Rubin, H. & Rubin, J. E. (1963) Equivalents of the Axiom of Choice. North-Holland, ISBN 9780444877086.Google Scholar
Sacchini, J. L. (2011) On Type-Based Termination and Dependent Pattern Matching in the Calculus of Inductive Constructions, PhD Thesis. France: ParisTech.Google Scholar
Sakai, M., Watanabe, Y. & Sakabe, T. (2001) An extension of dependency pair method for proving termination of higher-order rewrite systems. Ieice Trans. Inform. Syst. E84–D (8), 1025–1032.Google Scholar
Schmitz, S. (2014) Complexity Bounds for Ordinal-Based Termination (invited talk). In Proceedings of the 8th International Workshop on Reachability Problems. Lecture Notes in Computer Science, vol. 8762, pp. 1–19.Google Scholar
Scott, D. S. (1972) Continuous lattices. In Toposes, Algebraic Geometry and Logic, Lawvere, E. (ed), Lecture Notes in Mathematics, vol. 274. Springer, pp. 97–136.Google Scholar
Sellink, M. P. A. (1993) Verifying process algebra proofs in type theory. In Proceedings of the 1st International Workshop on Semantics of Specification Languages.Google Scholar
Sprenger, C. & Dam, M. (2003) On the structure of inductive reasoning: Circular and tree-shaped proofs in the μ-calculus. In Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 2620.Google Scholar
Sternagel, C. & Middeldorp, A. (2008) Root labeling. In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 5117. This paper contains errors described in Sternagel & Thiemann (2010).Google Scholar
Sternagel, C. & Thiemann, R. (2010) Signature extensions preserve termination – an alternative proof via dependency pairs. In Proceedings of the 24th International Conference on Computer Science Logic, Lecture Notes in Computer Science, vol. 6247.Google Scholar
Sulzmann, M. (2000) A General Framework for Hindley/Milner Type Systems with Constraints, PhD Thesis. USA: Yale University.Google Scholar
Sulzmann, M. (2001) A general type inference framework for Hindley/Milner style systems. In Proceedings of the 5th Fuji International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science, vol. 2024.Google Scholar
Szabo, M. E. (ed) (1969) Collected papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics, North-Holland, ISBN 9780444534194.Google Scholar
Tait, W. W. (1967) Intensional interpretations of functionals of finite type I. J. Symb. Log. 32 (2), 198–212.Google Scholar
Tarski, A. (1948) A Decision Method for Elementary Algebra and Geometry. Technical Report R-109. USA: RAND Corporation.Google Scholar
Tarski, A. (1955) A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285–309.Google Scholar
Telford, A. & Turner, D. (2000) Ensuring termination in ESFP. In Proceedings of the 15th British Colloquium for Theoretical Computer Science, Journal of Universal Computer Science, vol. 6(4).Google Scholar
TeReSe. (2003) Term rewriting systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press.Google Scholar
Termination competition. (2017) Accessed March 8, 2018. Available at: http://termination-portal.org/wiki/Termination_Competition.Google Scholar
Thiemann, R. & Giesl, J. (2005) The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput., 16 (4), 229–270.Google Scholar
THOR. (2014) Accessed March 8, 2018. Available at: http://www.cs.upc.edu/~albert/.Google Scholar
Turing, A. M. (1942) Available on http://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/KAMIN_LEVY/kamin-levy80spo.pdf. Some theorems about Church's system. Unpublished typescript reproduced in Gandy (1980a).Google Scholar
v. Heijenoort, J. (ed.) (1977) From Frege to Gödel, a Source Book in Mathematical Logic, 1879–1931. Harvard University Press.Google Scholar
van de Pol, J. (1993) Termination proofs for higher-order rewrite systems. In Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, vol. 816.Google Scholar
van de Pol, J. (1995) Two different strong normalization proofs? Computability versus functionals of finite type. In Proceedings of the 2nd International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science, vol. 1074.Google Scholar
van de Pol, J. (1996) Termination of Higher-Order Rewrite Systems, PhD Thesis. NL: Utrecht Universiteit.Google Scholar
van Oostrom, V. (1994) Confluence for Abstract and Higher-Order Rewriting, PhD Thesis. NL: Vrije Universiteit Amsterdam.Google Scholar
Wahlstedt, D. (2007) Dependent Type Theory with First-Order Parameterized Data Types and Well-Founded Recursion, PhD Thesis. Sweden: Chalmers University of Technology.Google Scholar
Walther, C. (1988) Argument-bounded algorithms as a basis for automated termination proofs. In Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 310.Google Scholar
Wanda. (2015) Accessed March 8, 2018. Available at: http://wandahot.sourceforge.net/.Google Scholar
Weiermann, A. (1998) How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: A case study. J. Symb. Log. 63 (4), 1348–1370.Google Scholar
Werner, B. (1994) Une Théorie Des Constructions Inductives, PhD Thesis. France: Université Paris 7.Google Scholar
Wilken, G. & Weiermann, A. (2012) Derivation lengths classification of gödel's T extending Howard's assignment. Log. Methods Comput. Sci. 8 (1), 1–44.Google Scholar
Xi, H. (2002) Dependent types for program termination verification. J. Higher-Order Symbol. Comput. 15 (1), 91–131.Google Scholar
Xi, H. (2003) Applied type system (extended abstract). In Proceedings of the International Workshop on Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 3085.Google Scholar
Xi, H., Chen, C. & Chen, G. (2003) Guarded recursive datatype constructors. In Proceedings of the 30th ACM Symposium on Principles of Programming Languages.Google Scholar
Zantema, H. (1995) Termination of term rewriting by semantic labelling. Fundam. Inform. 24, 89–105.Google Scholar
Zenger, C. (1997) Indexed types. Theor. Comput. Sci. 187 (1–2), 147–165.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.