Types-Decidability-Soundness.md

Decidability, Soundness and same stuff for Java/Scala type systems

Definitions

Sound algorithm

Complete algorithm

Decidable algorithm

Type inference Problem

Type checking Problem

Links

• Kennedy, Pierce, 2006, On Decidability of Nominal Subtyping with Variance
• Tate, Leung, Lerner, "Taming Wildcards in Java’s Type System" (final short version)
• Tate, Leung, Lerner, "Taming Wildcards in Java’s Type System" (previous long version)
• Undecidable type system leads to stack overflow
• JDK-4993221 : Produce infinite types from lub as required by JLS