Inhabitation of polymorphic and existential types

DOI10.1016/j.apal.2010.04.009zbMath1225.03034OpenAlexW1983087803MaRDI QIDQ636375

Makoto Tatsuta, Ryu Hasegawa, Hiroshi Nakano, Ken-etsu Fujita

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2010.04.009

zbMATH Keywords

quantifier eliminationsecond-order logictype theoryexistential typemagic formulassecond-order witness theoremtype inhabitation

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY ⋮ The existential fragment of second-order propositional intuitionistic logic is undecidable ⋮ Type checking and typability in domain-free lambda calculi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Typability and type checking in System F are equivalent and undecidable
• Non-strictly positive fixed points for classical natural deduction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic
• A simple proof of second-order strong normalization with permutative conversions
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Embedding first order predicate logic in fragments of intuitionistic logic
• Relational Parametricity and Control
• Typed Lambda Calculi and Applications