TITLE: Dependent types: the good, the bad and the ugly SPEAKER: Jaap Boender (Middlesex University) ABSTRACT: Over the last few months, I've been working on a Coq development that heavily involves dependent types - in a nutshell, types extended with terms, for example "all integers smaller than 42". In this talk, I'm going to explain what dependent types are, how they can be used, why they are the greatest thing since sliced bread and why they can be utterly frustrating at times, illustrated with examples from Coq and Matita (a theorem prover developed at the University of Bologna that deals with dependent types in a slightly different way).