Inhabitation of polymorphic and existential types

DOI10.1016/J.APAL.2010.04.009zbMATH Open1225.03034OpenAlexW1983087803MaRDI QIDQ636375FDOQ636375

Authors: 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

Recommendations

• scientific article; zbMATH DE number 2185726
• Inhabitation for non-idempotent intersection types
• The Inhabitation Problem for Non-idempotent Intersection Types
• Inhabitation of Low-Rank Intersection Types
• Inhabitation in Intersection and Union Type Assignment Systems

zbMATH Keywords

type theorysecond-order logicquantifier eliminationexistential typemagic formulassecond-order witness theoremtype inhabitation

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

• Polytypic values possess polykinded types
• Glivenko and Kuroda for simple type theory
• Polymorphism and apartness
• Type checking and typability in domain-free lambda calculi
• The existential fragment of second-order propositional intuitionistic logic is undecidable

This page was built for publication: Inhabitation of polymorphic and existential types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q636375)