D. Fridlender and M. Indrika, “Do we Need Dependent Types?”, BRICS, vol. 8, no. 10, Mar. 2001.