Abstract
This paper presents a reflection about function construction through well-founded recursion in the type theory known as Calculus of Inductive Constructions. It shows the expressive power of this calculus when dealing with concepts as accesibility and noetherianity among others. The properties of the General Recursion Scheme ([2]) and its relation with Structural Recursion in inductive types are analyzed. As a consequence, a methodology arises which is illustrated with some examples.We use the INRIA’s compiler of the Calculus of Inductive Constructions: Coq [6].
Government of Galicia, Spain, Project PGIDT02TIC00101CT and MCyT, Spain, Project TIC 2002-02859, and Xunta de Galicia, Spain, Project PGIDIT03PXIC10502PN.
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
Aczel, P.: Introduction to Inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North Holland, Amsterdam (1997)
Balaa, A.: Fonctions récursives générales dans le calcul des constructions. PhD. Theése. Université de Nice–Sophia Antipolis (2002)
Bertot, I., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)
Bove, A.: Simple General Recursion in Type Theory. Technical Report. Chalmers University of Technology, Goteborg (2000)
Coquand, T.: An Introduction to Type Theory. Notes of the FPCL summer school, Glasgow (1989)
Dowek, G., et al.: The Coq Proof Assistant Reference Manual. V8.0 INRIA 2004 (2004)
Nordström, B.: Terminating General Recursion. BIT 28 (1988)
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
Freire, J.L., Freire, E., Blanco, A. (2005). On Recursive Functions and Well–Founded Relations in the Calculus of Constructions. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds) Computer Aided Systems Theory – EUROCAST 2005. EUROCAST 2005. Lecture Notes in Computer Science, vol 3643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11556985_12
Download citation
DOI: https://doi.org/10.1007/11556985_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29002-5
Online ISBN: 978-3-540-31829-3
eBook Packages: Computer ScienceComputer Science (R0)