Bounded Quantification is Undecidable
Abstract
F≤ is a typed λ-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping.
Related papers
- Recursive subtyping for all JFP 2025
- A theory of higher-order subtyping with type intervals ICFP 2021
- Corrigendum: Decidable Bounded Quantification POPL 1995
- Structural Decidable Extensions of Bounded Quantification POPL 1995
- Decidable Bounded Quantification POPL 1994
- Greedy Implicit Bounded Quantification OOPSLA 2023
- Second-Order Hyperproperties CAV 2023
- Typed compilation of inclusive subtyping ICFP 2000