Abstract
We present a new method to specify a certain class of quotient in intentional type theory, and in the calculus of inductive constructions in particular. We define the notion of “normalized types”. The main idea is to associate a normalization function to a type, instead of the usual relation. This function allows to compute on a particular element for each equivalence class, avoiding the difficult task of computing on equivalence classes themselves. We restrict ourselves to quotients that allow the construction of such a function, i.e. quotient having a canonical member for each equivalence class. This method is described as an extension of the calculus of constructions allowing normalized types. We prove that this calculus has the properties of strong normalization, subject reduction, decidability of typing. In order to show the example of the definition of ℤ by a normalized type, we finally present a pseudo Coq session.
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
G. Barthe. Extensions of pure type systems. In proc TLCArs95, volume 902 of lncs. Springer-Verlag, 1995.
G. Barthe and H. Geuvers. Congruence types. In H. Kleine Buening, editor, Proc. Conf. Computer Science Logic, volume 1092 of Lecture Notes in Computer Science, pages 36–51, 1995.
F. Blanqui, J.-P. Jouannaud, and M. Okada. The Calculus of Algebraic Constructions. In Paliath Narendran and Michael Rusinowitch, editors, 10th International Conference on Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.
Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 14–25, Warsaw,Poland, June 1997. IEEE Comp. Soc. Press.
S. Boutin. Réflexions sur les quotients. thése d’université, Paris 7, April 1997.
Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, February 1988.
Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog’88, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
H. Geuvers. The church rosser property for βη-reduction in typed λ-calculi. In Proc. 7th IEEE Symp. Logic in Computer Science, Santa Cruz, pages 453–460, 1992.
M. Hofmann. Extensional concepts in intensional type theory. Phd thesis, Edinburgh university, 1995.
M. Hofmann. A simple model for quotient types. In proc TLCA’95, volume 902 of lncs. Springer-Verlag, 1995.
B. Jacobs. Quotients in simple type theory. Drafts and Notes. http://www.cwi. nl/ bjacobs/, 1991.
Christine Paulin-Mohring. Inductive definitions in the system COQ. In Typed Lambda Calculi and Applications, pages 328–345. Springer-Verlag, 1993. LNCS 664.
G. Malcolm R. Backhouse, P. Chisholm and E. Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1989.
Benjamin Werner. Méta-théorie du Calcul des Constructions Inductives. Thèse de doctorat, Univ. Paris VII, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Courtieu, P. (2001). Normalized Types. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_39
Download citation
DOI: https://doi.org/10.1007/3-540-44802-0_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42554-0
Online ISBN: 978-3-540-44802-0
eBook Packages: Springer Book Archive