Inhabitation for Intersection-Type Systems

For an intersection-type assignment system $\mathcal{T}$ and a type $\sigma$, the inhabitation problem asks whether there exists a closed lambda term $M$ such that $\vdash_{\mathcal{T}} M:\sigma$. Decide inhabitation for each model-oriented system listed in the source---HL, HR, Sc, CDZ, and DHM---and for the corresponding systems extended with recursive intersection types.