Typability and type checking in System F are equivalent and undecidable
type: Item
instance of: scholarly article
title: Typability and type checking in System F are equivalent and undecidable
zbMATH Open document ID: 0932.03017
DOI: 10.1016/S0168-0072(98)00047-5
author: J. B. Wells
published in: Annals of Pure and Applied Logic
publication date: 1999-09-22T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 1340811
zbMATH Keywords: type inference
zbMATH Keywords: System F
zbMATH Keywords: second-order polymorphically typed lambda calculus
zbMATH Keywords: typability
zbMATH Keywords: type checking
zbMATH Keywords: decidability
zbMATH Keywords: semi-unification
describes a project that uses: Haskell
describes a project that uses: ML
describes a project that uses: Miranda
describes a project that uses: Automath
MaRDI profile type: Publication
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q4023825
cites work: Q3142164
cites work: Q3994895
cites work: The undecidability of the second-order unification problem
cites work: Type inference in polymorphic type discipline
cites work: The complexity of type inference for higher-order typed lambda calculi
cites work: The Principal Type-Scheme of an Object in Combinatory Logic
cites work: The undecidability of the Turing machine immortality problem
cites work: Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
cites work: The undecidability of the semi-unification problem
cites work: Principality and type inference for intersection types using expansion variables
cites work: Finitely stratified polymorphism
cites work: Q3702495
cites work: Recursive unsolvability of Post's problem of ''Tag'' und other topics in theory of Turing machines
cites work: Polymorphic type inference and containment
cites work: Q3142167
cites work: Q5559220
cites work: Q3815293
cites work: Q4068054
cites work: The subtyping problem for second-order types is undecidable.
cites work: Q3721784
cites work: The emptiness problem for intersection types
cites work: Q4281489
cites work: Type reconstruction in Fω
description: scientific article; zbMATH DE number 1340811