Program of DTP

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