×

zbMATH — the first resource for mathematics

Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems. (English) Zbl 1286.68060
Summary: A multiple quantifier is a quantifier having inference rules that introduce or eliminate arbitrary number of quantifiers by one inference. This paper introduces the lambda calculus with negation, conjunction, and multiple existential quantifiers, and the lambda calculus with implication and multiple universal quantifiers. Their type checking and type inference are proved to be undecidable. This paper also shows that the undecidability of type checking and type inference in the type-free-style lambda calculus with negation, conjunction, and existence is reduced to the undecidability of type checking and type inference in the type-free-style polymorphic lambda calculus.
MSC:
68N18 Functional programming and lambda calculus
03B70 Logic in computer science
03B40 Combinatory logic and lambda calculus
PDF BibTeX XML Cite
Full Text: DOI