Why dependent types matter

We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system, using refinements of a well known program--merge sort--as a running example. We discuss its relationship with other proposals to introduce aspects of dependent types into functional programming languages and sketch some topics for further work in this area.

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: James McKinna
• Keywords: Functional Programming Languages, Interactive Program Development, POPL 2006, Programming Languages