Abstract
Type-based termination is a method to enforce termination of recursive definitions through a non-standard type system that introduces a notion of size for inhabitants of inductively defined types. The purpose of this tutorial is to provide a gentle introduction to a polymorphically typed λ-calculus with type-based termination, and to the size inference algorithm which is used to guarantee automatically termination of recursive definitions.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abel, A.: Termination Checking with Types. RAIRO – Theoretical Informatics and Applications 38(4), 277–319 (2004); Special Issue (FICS 2003)
Abel, A.: Type-Based Termination. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, LMU University, Munich (2006)
Abel, A.: Semi-Continuous Sized Types and Termination. LMCS 4(2-3) (2008)
Aczel, P.: An Introduction to Inductive Definitions. In: Barwise, J. (ed.) Handbook of mathematical logic. Studies in Logic and the Foundations of Mathematics, vol. 90, pp. 739–782. North-Holland, Amsterdam (1977)
Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-Based Termination of Recursive Definitions. Mathematical Structures in Computer Science 14(1), 97–141 (2004)
Barthe, G., Grégoire, B., Pastawski, F.: Practical Inference for Type-Based Termination in a Polymorphic Setting. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 71–85. Springer, Heidelberg (2005)
Chin, W.-N., Khoo, S.-C.: Calculating Sized Types. Higher-Order and Symbolic Computation 14(2-3), 261–300 (2001)
Coquand, T., Dybjer, P.: Inductive Definitions and Type Theory: an Introduction (Preliminary Version). In: Thiagarajan, P.S. (ed.) FSTTCS 1994. LNCS, vol. 880, pp. 60–76. Springer, Heidelberg (1994)
Gallier, J.H.: What’s So Special About Kruskal’s Theorem and the Ordinal Γ0? A Survey of Some Results in Proof Theory. Annals of Pure and Applied Logic 53(3), 199–260 (1991)
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)
Girard, J.-Y.: Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur. PhD thesis, Université Paris 7 (1972)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)
Hughes, J., Pareto, L., Sabry, A.: Proving the Correctness of Reactive Systems Using Sized Types. In: Proceedings of POPL 1996, pp. 410–423. ACM, New York (1996)
Mendler, N.P.: Recursive Types and Type Constraints in Second Order Lambda-Calculus. In: Proceedings of LiCS 1987, pp. 30–36. IEEE Computer Society, Los Alamitos (1987)
Parigot, M.: On the Representation of Data in Lambda-Calculus. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 309–321. Springer, Heidelberg (1990)
Spławski, Z., Urzyczyn, P.: Type Fixpoints: Iteration vs. Recursion. In: Proceedings of ICFP 1999, pp. 102–113. ACM, New York (1999)
Steffen, M.: Polarized Higher-order Subtyping. PhD thesis, Department of Computer Science, University of Erlangen (1997)
Tait, W.W.: A Realizability Interpretation of the Theory of Species. In: Parikh, R. (ed.) Logic Colloquium. LNCS, vol. 453, pp. 240–251. Springer, Heidelberg (1975)
Xi, H.: Dependent Types for Program Termination Verification. Higher-Order and Symbolic Computation 15(1), 91–131 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Barthe, G., Grégoire, B., Riba, C. (2009). A Tutorial on Type-Based Termination. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds) Language Engineering and Rigorous Software Development. LerNet 2008. Lecture Notes in Computer Science, vol 5520. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03153-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-03153-3_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03152-6
Online ISBN: 978-3-642-03153-3
eBook Packages: Computer ScienceComputer Science (R0)