CJTCS Special Issue: CATS 2009
Selected papers from
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.
Published by Dept. CS U. Chicago. Copyright 2010 CJTCS and the author.
Type Checking and Inference
Polymorphic and Existential Types
in Multiple-Quantifier and Type-Free Systems
Graduate School of Informatics,
Kyoto 606-8501, Japan
National Institute of Informatics,
2-1-2 Hitotsubashi, Tokyo 101-8430, Japan
June 24, 2010
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)
Special Issue, Article 6
CATS2009 Special Issue