Typability and type checking in System F are equivalent and undecidable

DOI10.1016/S0168-0072(98)00047-5zbMath0932.03017MaRDI QIDQ1302292

J. B. Wells

Publication date: 22 September 1999

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

zbMATH Keywords

decidabilitytype inferencetypabilitytype checkingSystem Fsecond-order polymorphically typed lambda calculussemi-unification

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Related Items (22)

The role of polymorphism in the characterisation of complexity by soft types ⋮ Principality and type inference for intersection types using expansion variables ⋮ A decidable theory of type assignment ⋮ Light affine lambda calculus and polynomial time strong normalization ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ The subtyping problem for second-order types is undecidable. ⋮ Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version) ⋮ Inhabitation of polymorphic and existential types ⋮ A System F with Call-by-Name Exceptions ⋮ No value restriction is needed for algebraic effects and handlers ⋮ Unnamed Item ⋮ Type checking and typability in domain-free lambda calculi ⋮ The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types ⋮ Type inference for light affine logic via constraints on words ⋮ Iteration and coiteration schemes for higher-order and nested datatypes ⋮ Unnamed Item ⋮ Existential Type Systems with No Types in Terms ⋮ Recasting ML\(^{\text F}\) ⋮ Enhanced type inference for binding-time analysis ⋮ Intersection, Universally Quantified, and Reference Types ⋮ Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions ⋮ Typability and type checking in System F are equivalent and undecidable

Uses Software

• ML
• Haskell
• Miranda
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Polymorphic type inference and containment
• The undecidability of the second-order unification problem
• Finitely stratified polymorphism
• Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
• The undecidability of the semi-unification problem
• Typability and type checking in System F are equivalent and undecidable
• The subtyping problem for second-order types is undecidable.
• Principality and type inference for intersection types using expansion variables
• Type reconstruction in F_ω
• The complexity of type inference for higher-order typed lambda calculi
• The emptiness problem for intersection types
• Type inference in polymorphic type discipline
• The undecidability of the Turing machine immortality problem
• The Principal Type-Scheme of an Object in Combinatory Logic

This page was built for publication: Typability and type checking in System F are equivalent and undecidable