Typability and type checking in System F are equivalent and undecidable

DOI10.1016/S0168-0072(98)00047-5zbMATH Open0932.03017MaRDI QIDQ1302292FDOQ1302292

Authors: J. B. Wells 

Publication date: 22 September 1999

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

Recommendations

• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F
• The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types
• The subtyping problem for second-order types is undecidable.
• Type checking and typability in domain-free lambda calculi
• scientific article; zbMATH DE number 512796

zbMATH Keywords

decidabilitytypabilitytype checkingSystem Ftype inferencesecond-order polymorphically typed lambda calculussemi-unification

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (31)

• Existential type systems between Church and Curry style (type-free style)
• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F
• Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)
• Enhanced type inference for binding-time analysis
• The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types
• Bounded quantification is undecidable
• The role of polymorphism in the characterisation of complexity by soft types
• Type inference for light affine logic via constraints on words
• The subtyping problem for second-order types is undecidable.
• Light affine lambda calculus and polynomial time strong normalization
• Typability and type checking in System F are equivalent and undecidable
• Recasting ML\(^{\text F}\)
• Title not available (Why is that?)
• A System F with Call-by-Name Exceptions
• Scrap Your Type Applications
• Principality and type inference for intersection types using expansion variables
• Intersection, Universally Quantified, and Reference Types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
• Undecidability of equality for codata types
• Inhabitation of polymorphic and existential types
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Existential Type Systems with No Types in Terms
• Type checking and typability in domain-free lambda calculi
• A decidable theory of type assignment
• Iteration and coiteration schemes for higher-order and nested datatypes
• Title not available (Why is that?)
• Title not available (Why is that?)
• No value restriction is needed for algebraic effects and handlers
• Title not available (Why is that?)

Uses Software

• ML
• Haskell
• Miranda
• Automath

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

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