Bounded quantification is undecidable

DOI10.1006/inco.1994.1055zbMath0794.03023OpenAlexW2792739471MaRDI QIDQ1327694

Benjamin C. Pierce

Publication date: 20 June 1994

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/17db237c8d54b0701ddac961860ef91ee6e2c0e8

zbMATH Keywords

reduction from the halting problem for two-counter Turing machinestyped \(\lambda\)-calculus with subtyping and bounded second-order polymorphism

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Combinatory logic and lambda calculus (03B40)

Related Items (13)

Principality and type inference for intersection types using expansion variables ⋮ Bounded existentials and minimal typing ⋮ Higher-order subtyping ⋮ The subtyping problem for second-order types is undecidable. ⋮ A calculus with recursive types, record concatenation and subtyping ⋮ Divergence of \(F_{\leq}\) type checking ⋮ On the decidability of subtyping with bounded existential types and implementation constraints ⋮ Subtyping recursion and parametric polymorphism in kernel Fun ⋮ Recasting ML\(^{\text F}\) ⋮ Basic theory of \(F\)-bounded quantification. ⋮ Comparing object encodings. ⋮ Type destructors ⋮ Foundations for virtual types

This page was built for publication: Bounded quantification is undecidable