Abstract
There are several approaches to the problem of giving a categorical semantics to Martin-Löf type theory with dependent sums and products and extensional equality types. The most established one relies on the notion of a type-category (or category with attributes) with \({\it \Sigma}\) and \({\it \Pi}\) types. We extend such a semantics by introducing coinductive types both on the syntactic level and in a type-category. Soundness of the semantics is preserved.
As an example of such a category, we prove that the type-category built over a locally cartesian closed category \({\mathcal C}\) admits coinductive types whenever \({\mathcal C}\) has final coalgebras for all polynomial functors.
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.
Similar content being viewed by others
References
Abbott, M., Altenkirch, T., Ghani, N.: Representing strictly positive types. Presented at APPSEM annual meeting, invited for submission to Theoretical Computer Science (2004)
Aczel, P.: Non-Well-Founded Sets. In: Center for the Study of Language and Information. CSLI Lecture Notes, vol. 14. Stanford University, Stanford (1988)
Aczel, P., Adámek, J., Milius, S., Velebil, J.: Infinite trees and completely iterative theories: a coalgebraic view. Theoretical Computer Science 300, 1–45 (2003)
Altenkirch, T.: Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science (LICS 1999), pp. 412–421. IEEE, Los Alamitos (1999)
Barr, M.: Terminal coalgebras for endofunctors on sets (1999), Available from ftp://www.math.mcgill.ca/pub/barr/trmclgps.zip
Bénabou, J.: Fibered categories and the foundations of naive category theory. J. Symbolic Logic 50(1), 10–37 (1985)
Cartmell, J.: Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic 32(3), 209–243 (1986)
Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994)
Gaspes, V.: Infinite objects in type theory (1997)
Hallnäs, L.: On the syntax of infinite objects: an extension of Martin-Löf’s theory of expressions. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 94–104. Springer, Heidelberg (1990)
Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427–441. Springer, Heidelberg (1995)
Jacobs, B.: Categorical logic and type theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North-Holland Publishing Co., Amsterdam (1999)
Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS 62, 222–259 (1996)
Lindström, I.: A construction of non-well-founded sets within Martin-Löf’s type theory. Journal of Symbolic Logic 54(1), 57–64 (1989)
Martin-Löf, P.: Intuitionistic type theory. Studies in Proof Theory. Lecture Notes, vol. 1. Bibliopolis, Naples (1984)
Martin-Löf, P.: Mathematics of infinity. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 146–197. Springer, Heidelberg (1990)
Mendler, N.P., Panangaden, P., Constable, R.L.: Infinite objects in type theory. In: Symposium on Logic in Computer Science (LICS 1986), pp. 249–257. IEEE Computer Society Press, Los Alamitos (1986)
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s type theory. International Series of Monographs on Computer Science, vol. 7. The Clarendon Press/Oxford University Press (1990)
Pitts, A.M.: Categorical logic. Handbook of logic in computer science, vol. 5, pp. 39–128. Oxford Sci. Publ./Oxford Univ. Press (2000)
Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95(1), 33–48 (1984)
Streicher, T.: Semantics of type theory. Progress in Theoretical Computer Science. Birkhäuser (1991); Correctness, completeness and independence results
Turi, D., Rutten, J.: On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces. Mathematical Structures in Computer Science 8(5), 481–540 (1998)
van den Berg, B., De Marchi, F.: Non-well-founded trees in categories, Available online at http://arxiv.org/abs/math.CT/0409158 (submitted)
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
De Marchi, F. (2005). On the Semantics of Coinductive Types in Martin-Löf Type Theory. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds) Algebra and Coalgebra in Computer Science. CALCO 2005. Lecture Notes in Computer Science, vol 3629. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11548133_8
Download citation
DOI: https://doi.org/10.1007/11548133_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28620-2
Online ISBN: 978-3-540-31876-7
eBook Packages: Computer ScienceComputer Science (R0)