| 18.00 | Pub the Three Wheatsheves |
| 09.00 | Registration and Welcome |
| 09.30 | Why dependent types matter |
| Thorsten Altenkirch (University of Nottingham) | |
| 10.00 | Dependently Typed DSLs for Resource Usage Verification |
| Edwin Brady (University of St. Andrews) | |
| 10.30 | Coffee |
| 11.00 | Ecce isn't Epigram2 |
| Peter Morris (University of Nottingham) | |
| 11.30 | Dependent Finger Trees |
| Matthieu Sozeau (LRI) | |
| 12.00 | Lunch in the Restaurant |
| 14.00 | Derivation-Carrying Code using Dependent Types |
| Shin-Cheng Mu (Academia Sinica, Taiwan) | |
| 14.30 | Interactive Programs and Coalgebras |
| Anton Setzer (Swansea University) | |
| 15.00 | Coffee and Discussion |
| 16.00 | Supporting the Development of Dependently Typed Functional Programs |
| Sean Wilson (Edinburgh University) | |
| 16.15 | Talk 'Bout Agda |
| Ulf Norell (Chalmers University of Technology) | |
| 16.45 | Structurally Recursive Descent Parsing |
| Nils-Anders Danielsson (University of Nottingham) | |
| 17.15 | Close |
| 09.00 | Programming a compiler with a proof assistant: an experience report (invited talk) |
| Xavier Leroy (INRIA, Paris-Rocquencourt) | |
| 10.00 | Verifying a Semantic beta-eta-Conversion Test for Martin-Loef Type Theory |
| Andreas Abel (University of Munich) | |
| 10.30 | Coffee |
| 11.00 | A core theory for Dependently Typed Programming |
| Nicholas Oury (University of Nottingham) | |
| 11.30 | Delphin: Practical programming with HOAS and Dependent Types |
| Adam Poswolsky (Yale University) | |
| 12.00 | Lunch in the Restaurant |
| 14.00 | Programming with nested datatypes through dependent types |
| Ralph Matthes (IRIT (CNRS and University of Toulouse III)) | |
| 14.30 | Machine-Independent Code Certification with the LF Type Theory |
| Nicholas Magaud (University of Strasbourg) | |
| 15.00 | Coffee and Discussion |
| 16.00 | TBA |
| Stephanie Weirich (CMU) | |
| 16.15 | Can dependently typed programming succeed? (invited talk) |
| Lennart Augustsson (Credit Suisse) | |
| 17.15 | Close |
| 19.30 | Conference Dinner in the Restaurant |
| 09.00 | Polarity and duality in type theory |
| Noam Zeilberger (CMU) | |
| 09.30 | Power of Pi |
| Wouter Swierstra (University of Nottingham) | |
| 10.00 | The Implicit Calculus of Constructions (ICC*) |
| Bruno Bernardo (Ecole polytechnique, INRIA Futurs) | |
| 10.30 | Coffee |
| 11.00 | Dependent Types for Modelling and Simulation: Challenges and Opportunities |
| Henrik Nilsson (University of Nottingham) | |
| 11.30 | Generalizing Dependent Inductive Datatypes to Specify the Static Semantics of Programming Languages |
| Christian Stork (UCI) | |
| 12.00 | Data, Deliberately |
| Conor McBride (Alta Systems) | |
| 12.30 | Close |