Abstract
We study the typability in a partial higher order typed lambda-calculus which generalizes Girard's system F ω . A set of equations between kinded constructors is associated to each term of the system whose unification gives the possible typings. We define a syntactic restriction on constructors which is enough to capture all the typability problems: the elementary calculus. We use these principal typed terms to prove that the higher order typings hierarchy collapse at the second level.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Boehm, H. J.: Partial polymorphic type inference is undecidable. 26th Annual Symposium on Foundations of Computer Science IEEE Press (1985) 339–345
Gallier, J. H.: On Girard's Candidats de Reductibilite. Logic and Computer Science Academic Press P. Odifreddi (1990) 123–204
Giannini, P., Ronchi Della Rocca, S.: Characterization of typings in polymorphic type disscipline. Proc. 3rd Ann. Symp. Logic Comput. Sci. Edinburgh (1988) 61–70
Giannini, P., Honsell, F., Ronchi Della Rocca, S.: Type Inference: Some results, Some problems. Fondamenta Informaticae 19(1,2) (1993) 87–125
Girard, J.Y.: Interpretation Fonctionnelle et Elimination des Coupures de l'Arithmétique d'Ordre Supérieure. Thèse d'etat Université Paris VII (1972)
Goldfarb, W.: The Undecidability of the Second-Order Unification Problem. TCS 13 (1981) 225–230
Gould, W. E.: A Matching Procedure for Omega-Order Logic. Princeton University (1966)
Hindley, J. R.: The Principal Type Scheme of an Object in Combinatory Logic. Trans. Am. Math. Soc. 146 (1969) 29–60
Huet, G.: The Undecidability of Unification in Third-Order Logic. Information and Control (22) (1973) 257–267
Malecki, S.: Quelques Résultats sur la Typabilité dans le Système F. Thèse de Doctorat Université Paris VII (1992)
Pfenning, F.: Partial polymorphic type inference and higher order unification. ACM LISP and Functional Programming Conference (1988) 153–163
Reynolds, J. C.: Towards a Theory of Type Structures. Paris Colloquium on Programming, Springer-Verlag, (1974) 408–425
Snyder, W.: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic (1991)
Urzyczyn, P.: Type reconstruction in F ω is undecidable. Int'l Conf. Typed Lambda Calculi and Applications Springer-Verlag 664 (1993) 418–432
Wells, J.B.: Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable. Eight Annual IEEE Symposium on Logic in Computer Science IEEE Press (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Malecki, S. (1997). Proofs in system F ω can be done in system F 1ω . In: van Dalen, D., Bezem, M. (eds) Computer Science Logic. CSL 1996. Lecture Notes in Computer Science, vol 1258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63172-0_46
Download citation
DOI: https://doi.org/10.1007/3-540-63172-0_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63172-9
Online ISBN: 978-3-540-69201-0
eBook Packages: Springer Book Archive