zbMATH — the first resource for mathematics

Type checking and typability in domain-free lambda calculi. (English) Zbl 1241.03011
Summary: This paper shows (1) the undecidability of type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic lambda calculus, and (3) the undecidability of type checking and the typability problems in the domain-free lambda calculus with function and existential types. The first and the third results are proved by the second result and CPS translations that reduce those problems in the domain-free polymorphic lambda calculus to those in the domain-free lambda calculi with existential types. The key idea is the conservativity of the domain-free lambda calculi with existential types over the images of the translations.
03B40 Combinatory logic and lambda calculus
Full Text: DOI
[1] Barthe, G.; Sørensen, M.H., Domain-free pure type systems, Journal of functional programming, 10, 412-452, (2000) · Zbl 0979.03013
[2] Danvy, O.; Filinski, A., Representing control: a study of the CPS translation, Mathematical structures in computer science, 2, 4, 361-391, (1992) · Zbl 0798.68102
[3] Fujita, K., Explicitly typed \(\lambda \mu\)-calculus for polymorphism and call-by-value, (), 162-177 · Zbl 0933.03009
[4] Fujita, K.; Schubert, A., Partially typed terms between church-style and curry-style, (), 505-520 · Zbl 0998.03009
[5] Fujita, K., Galois embedding from polymorphic types into existential types, (), 194-208 · Zbl 1114.03009
[6] Fujita, K.; Schubert, A., Existential type systems with no types in terms, (), 112-126 · Zbl 1246.03028
[7] J.Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de doctorat d’Etat, Université de Paris VII, 1972.
[8] Harper, R.; Lillibridge, M., Polymorphic type assignment and CPS conversion, Lisp and symbolic computation, 6, 361-380, (1993)
[9] Hasegawa, M., Relational parametricity and control, Logical methods in computer science, 2, 3:3, 1-22, (2006) · Zbl 1126.68023
[10] M. Hasegawa, 2007 (unpublished manuscript).
[11] Mitchell, J.C.; Plotkin, G.D., Abstract types have existential type, ACM transactions on programming languages and systems, 10, 3, 470-502, (1988)
[12] E. Moggi, Computational lambda-calculus and monads, in: Proceedings of 4th Annual Symposium on Logic in Computer Science, LICS 1989, 1989, pp. 14-23. · Zbl 0716.03007
[13] Nakazawa, K., An isomorphism between cut-elimination procedure and proof reduction, (), 336-350 · Zbl 1215.03067
[14] Nakazawa, K.; Tatsuta, M.; Kameyama, Y.; Nakano, H., Undecidability of type-checking in domain-free typed lambda-calculi with existence, (), 477-491
[15] Parigot, M., \(\lambda \mu\)-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[16] Plotkin, G., Call-by-name, call-by-value, and the \(\lambda\)-calculus, Theoretical computer science, 1, 125-159, (1975) · Zbl 0325.68006
[17] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[18] Sabry, A.; Wadler, P., A reflection on call-by-value, ACM transactions on programming languages and systems, 19, 6, 916-941, (1997)
[19] Sørensen, M.H.; Urzyczyn, P., A syntactic embedding of predicate logic into second-order propositional logic, Notre dame journal of formal logic, 51, 4, 457-473, (2010) · Zbl 1216.03029
[20] Tatsuta, M.; Fujita, K.; Hasegawa, R.; Nakano, H., Inhabitation of polymorphic and existential types, Annals of pure and applied logic, 161, 1390-1399, (2010) · Zbl 1225.03034
[21] H. Thielecke, Categorical structure of continuation passing style, Ph.D. Thesis, University of Edinburgh, 1997.
[22] von Plato, J., Natural deduction with general elimination rules, Archive for mathematical logic, 40, 541-567, (2001) · Zbl 1021.03050
[23] Wells, J.B., Typability and type checking in system \(F\) are equivalent and undecidable, Annals of pure and applied logic, 98, 111-156, (1999) · Zbl 0932.03017
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.