2009 Computing: The Australasian Theory Symposium

held in Wellington, New Zealand January 20-23 2009.

Guest Editors: Rod Downey, Victoria University of Wellington, NZ

Prabhu Manyem, Shanghai University, PRC.

Article 2010-10

Type Checking and Inference
for Polymorphic and Existential Types
in Multiple-Quantifier and Type-Free Systems

Koji Nakazawa
Graduate School of Informatics,
Kyoto University,
Kyoto 606-8501, Japan
E-mail:tt knak@kuis.kyoto-u.ac.jp
and
Makoto Tatsuta
National Institute of Informatics,
2-1-2 Hitotsubashi, Tokyo 101-8430, Japan
E-mail: tatsuta@nii.ac.jp

June 24, 2010

Abstract

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.

The article: PDF (232,892 bytes)
Source materials: ZIP (55,242 bytes)
Self citation in BIBTeX (345 bytes)
Original version: PDF (199,993 bytes)

DOI: 10.4086/cjtcs.2010.010