Friday, July 9th
Friday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
| 09:00 | Ana Bove (Chalmers University) 10 Years of Partiality and General Recursion |
10:30‑12:30 Session 1
| 10:30 | Andreas Abel (University of Munich) Parametric Dependent Function Types |
| 11:00 | Edwin Brady (University of St Andrews) Practical, efficient programming with dependent types |
| 11:30 | Anton Setzer (University of Swansea) Coalgebras in dependent type theory |
| 12:00 | Nils Anders Danielsson (University of Nottingham) Operational Semantics Using the Partiality Monad |
14:00‑15:00 Session 2
| 14:00 | Darin Morrison (University of Nottingham) Mechanizing Metatheory via Dependently Typed Programming |
| 14:30 | Antonis Stampoulis (Yale University) VeriML: Type-safe computation of logical terms inside a language with effects |
15:30‑17:00 Session 3
| 15:30 | Carsten Schuermann (IT University Copenhagen) The HOL-Nuprl connection in Delphin |
| 16:00 | Brigitte Pientka (McGill University) Type reconstruction in dependently typed programming |
| 16:30 | Dan Licata (Carnegie Mellon University) Security-Typed Programming within Dependently Typed Programming |
Saturday, July 10th
Saturday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Invited Talk
| 09:00 | Matthieu Sozeau (Harvard University) Elaborations in Type Theory |
10:30‑12:30 Session 4
| 10:30 | Adam Chlipala (Harvard University) Generating Pieces of Web Applications with Type-Level Programming |
| 11:00 | Larry Diehl Unit & integration test composition via lemmas |
| 11:30 | Sean Wilson (University of Edinburgh) Supporting Dependently Typed Functional Programming with Proof Automation and Testing |
| 12:00 | Karim Kariso (University of Swansea) Integrating Agda and Automated Theorem Proving Techniques |
14:00‑15:00 Session 5
| 14:00 | Cezar Ionescu (Potsdam Institute for Climate Impact Research) Using dependent types in models of climate change impacts |
| 14:30 | Hugo Herbelin (INRIA) A sequent calculus presentation of the Calculus of Inductive Constructions |
15:30‑17:00 Session 6
| 15:30 | Makoto Hamana (University of Gunma) Another Initial Algebra Semantics of Inductive Families for Programming |
| 16:00 | Tarmo Uustalu (Institute of Cybernetics, Tallinn) Safely navigable datastructures with cycles and sharing |
| 16:30 | Ulf Norell (Chalmers University) Lightweight reflection in Agda |