Here's a video of Conor McBride's ICFP talk, as mentioned by Edwin last night: http://www.quora.com/Programming-Languages/What-are-the-killer-applications-for-dependent-types-in-general-purpose-programming-languages?srid=uIE&st=ns I hope you're all feeling less groggy than me! Miles