Abstract
We introduce a polymorphic λ-calculus that features inductive types and that enforces termination of recursive definitions through typing. Then, we define a sound and complete type inference algorithm that computes a set of constraints to be satisfied for terms to be typable. In addition, we show that Subject Reduction fails in a naive use of typed-based termination for a λ-calculus à la Church, and we propose a general solution to this problem.
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
Abel, A.: Termination checking with types. RAIRO– Theoretical Informatics and Applications 38, 277–320 (2004)
Amadio, R., Coupet-Grimal, S.: Analysis of a guard condition in type theory. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 48–62. Springer, Heidelberg (1998)
Bac, A.: Un algorithme d’inférence de types pour les types coinductifs. Master’s thesis, École Normale Supérieure de Lyon (1998)
Barras, B.: Auto-validation d’un système de preuves avec familles inductives. PhD thesis, Université Paris 7 (1999)
Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14, 97–141 (2004)
Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 24–39. Springer, Heidelberg (2004)
Chin, W.-N., Khoo, S.-C.: Calculating sized types. Higher-Order and Symbolic Computation 14(2-3), 261–300 (2001)
Coq Development Team. The Coq Proof Assistant User’s Guide. Version 8.0 (January 2004)
Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Nordström, B., Pettersson, K., Plotkin, G. (eds.) Informal proceedings of Logical Frameworks 1992, pp. 193–217 (1992)
Giménez, E.: Un calcul de constructions infinies et son application à la vérification de systèmes communicants. PhD thesis, Ecole Normale Superieure de Lyon (1996)
Giménez, E.: Structural recursive definitions in Type Theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397–408. Springer, Heidelberg (1998)
Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proceedings of POPL 1996, pp. 410–423. ACM Press, New York (1996)
Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51(1-2), 159–172 (1991)
Steffen, M.: Polarized Higher-order Subtyping. PhD thesis, Department of Computer Science, University of Erlangen (1997)
Werner, B.: Méta-théorie du Calcul des Constructions Inductives. PhD thesis, Université Paris 7 (1994)
Xi, H.: Dependent Types for Program Termination Verification. In: Proceedings of LICS 2001, pp. 231–242. IEEE Computer Society Press, Los Alamitos (2001)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of POPL 1999, pp. 214–227. ACM Press, New York (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Grégoire, B., Pastawski, F. (2005). Practical Inference for Type-Based Termination in a Polymorphic Setting. In: Urzyczyn, P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_7
Download citation
DOI: https://doi.org/10.1007/11417170_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25593-2
Online ISBN: 978-3-540-32014-2
eBook Packages: Computer ScienceComputer Science (R0)