×

zbMATH — the first resource for mathematics

Existential type systems with no types in terms. (English) Zbl 1246.03028
Curien, Pierre-Louis (ed.), Typed lambda calculi and applications. 9th international conference, TLCA 2009, Brasilia, Brazil, July 1–3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02272-2/pbk). Lecture Notes in Computer Science 5608, 112-126 (2009).
Summary: We study type checking, typability, and type inference problems for type-free-style and Curry-style second-order existential systems where the type-free style differs from the Curry style in that the terms of the former contain information on where the existential quantifier elimination and introduction take place but omit the information on which types are involved. We show that all the problems are undecidable employing reduction of second-order unification in case of the type-free system and semiunification in case of the Curry style system. This provides a fine border between problems yielding to a reduction of second-order unification problem and the semiunification problem. In addition, we investigate the subject reduction property of the system in the Curry-style.
For the entire collection see [Zbl 1165.03001].

MSC:
03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
03B70 Logic in computer science
Software:
Automath
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andou, Y.: A normalization-procedure for the first order classical natural deduction with full logical symbols. Tsukuba Journal of Mathematics 19(1), 153–162 (1995) · Zbl 0835.03021
[2] Barendregt, H.: Lambda Calculi with Types. In: Handbook of Logic in Computer Science, vol. II. Oxford University Press, USA (1993) · Zbl 0796.03020
[3] Boehm, H.-J.: Partial polymorphic type inference is undecidable. In: 26th Annual Symposium on Foundations of Computer Science, pp. 339–345. IEEE, Los Alamitos (1985)
[4] Barthe, G., Sørensen, M.H.: Domain-free pure type systems. J. Functional Programming 10, 412–452 (2000) · Zbl 0979.03013 · doi:10.1017/S0956796800003750
[5] Fujita, K., Schubert, A.: Partially typed terms between Church-style and Curry-style. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 505–520. Springer, Heidelberg (2000) · Zbl 0998.03009 · doi:10.1007/3-540-44929-9_35
[6] Fujita, K.: CPS-translation as adjoint (submitted) · Zbl 1186.68101
[7] Fujita, K.: Galois embedding from polymorphic types into existential types. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 194–208. Springer, Heidelberg (2005) · Zbl 1114.03009 · doi:10.1007/11417170_15
[8] Hasegawap, M.: Relational parametricity and control. LMCS 2, 3 (2006)
[9] Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: The undecidability of the semi-unification problem. In: STOC 1990: Proceedings of the twenty-second annual ACM symposium on Theory of computing, pp. 468–476. ACM Press, New York (1990) · Zbl 0769.68059 · doi:10.1145/100216.100279
[10] Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst. 15(2), 290–311 (1993) · doi:10.1145/169701.169687
[11] Mairson, H.G.: Deciding ML typability is complete for deterministic exponential time. In: POPL 1990: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 382–401. ACM Press, New York (1990)
[12] Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10(3), 470–502 (1988) · doi:10.1145/44501.45065
[13] Nakazawa, K., Tatsuta, M., Kameyama, Y., Nakano, H.: Undecidability of type-checking in domain-free typed lambda-calculi with existence. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 478–492. Springer, Heidelberg (2008) · Zbl 1156.03316 · doi:10.1007/978-3-540-87531-4_34
[14] Pfenning, F.: On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae 19(1,2), 185–199 (1993) · Zbl 0789.03017
[15] Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965) · Zbl 0173.00205
[16] Schubert, A.: Second-order unification and type inference for Church-style polymorphism. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 279–288. ACM Press, New York (1998)
[17] Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 149. Elsevier Science Inc., New York (2006) · Zbl 1183.03004
[18] Wells, J.B.: Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Logic 98(1–3), 111–156 (1999) · Zbl 0932.03017 · doi:10.1016/S0168-0072(98)00047-5
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.