The Inhabitation Problem for Rank Two Intersection Types

Dariusz Kusmierek

We prove that the inhabitation problem for rank two intersection types is decidable, but (contrary to common belief) EXPTIME-hard. The exponential time hardness is shown by reducti…