Abstract
We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt's typed λ-cube [1] via a natural type erasing function E, that erases type information from terms. We prove that the systems in the former cube enjoy good computational properties, like subject reduction and strong normalization. We study the relationship between the two cubes, which leads to some unexpected results in the field of systems with dependent types.
Supported by the Netherlands Organisation for the Advancement of Pure Research (N.W.O.).
Partly supported by HCM project No. ERBCHRXCT920046 “Typed Lambda Calculus”
Partly supported by grants NSF CCR-9113196, KBN 2 1192 91 01 and by a grant from the Commission of The European Communities ERB-CIPA-CT92-2266(294).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barendregt, H.P., Lambda Calculi with Types, Handbook of Logic in Computer Science, Abramsky, Gabbai, Maibaum eds., Oxford University Press, 1991.
Barendregt, H.P., Introduction to Generalised Type Systems, Journal of Functional Programming, volume 1(2), 125–154, 1991.
Berardi, S., Towards a Mathematical Analysis of Type Dependence in Coquand-Huet Calculus of Constructions and the Other Systems in Barendregt's Cube, Department of Computer Science, CMU, and Dipartimento di Matematica, Torino, 1988.
Curry, H.B., Modified Basic Functionality in Combinatory Logic, Dialectica, 1969.
Coquand, T., Metamathematical Investigations of a Calculus of Constructions, Logic and Computer Science, Odifreddi ed., Academic Press, 91–122, 1990.
Coquand, T. and Huet, G., The Calculus of Constructions, Information and Computation, 76(2,3), 95–120, 1988.
Dowek, G., The Undecidability of Typability in the Lambda-Pi-Calculus, Proc. Typed Lambda Calculi and Applications, LNCS 664, 139–145, 1993.
Geuvers, H. and Nederhof, M., Modular Proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming, 1(2), 155–189, 1991.
Giannini, P. and Ronchi Della Rocca, S., Characterization of Typings in Polymorphic Type Discipline, Proc. Logic in Computer Science, IEEE, 61–70, 1988.
Giannini, P., Honsell, F. and Ronchi Della Rocca, S., Type Inference: Some Results, Some Problems, Fundamenta Informaticae, 19(1,2), pp.87–126, 1993.
Girard, J.Y., The System F of Variable Types, Fifteen Years Later, Theoretical Computer Science, 45, 159–192, 1987.
Harper, B., Honsell, F. and Plotkin, G., A Framework for Defining Logics, Journal of the ACM, 40, 1993.
Klop, J. W., Combinatory Reduction Systems, PhD-thesis, Rijksuniversiteit Utrecht, 1980.
Leivant, D., Polymorphic Type Inference, In Symposium on Principles of Programming Languages, ACM, 88–98, 1983.
Reynolds, J.C., Towards a Theory of Type Structures, Proc. Paris Colloquium on Programming, Springer Verlag, 408–425, 1974.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Bakel, S., Liquori, L., della Rocca, S.R., Urzyczyn, P. (1994). Comparing cubes. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_33
Download citation
DOI: https://doi.org/10.1007/3-540-58140-5_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58140-6
Online ISBN: 978-3-540-48442-4
eBook Packages: Springer Book Archive