Abstract
The third seminar continued the exploration of programming with dependent types begun at the first seminar. The speaker identified two major pitfalls for programming in a type theory like Coq's : partiality and non-termination, and showed how the use of dependent types makes it possible to make functions total and to demonstrate termination. There is, however, the problem of dependent filtering, i.e. case analysis on these dependent types, which is more complex than the usual non-dependent filtering.
