Inhabitation of polymorphic and existential types

DOI10.1016/J.APAL.2010.04.009MaRDI QIDQ636375zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(5)

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

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)