Program


Session 1
9:00-10:00 Edwin Brady Programming with Dependent Types[slides]
10:00-10:30 Coffee Break
Session 2
10:30-11:00 Bob Atkey Reifying Parametricity[slides]
11:00-11:30 Steven Keuchel Generic Programming with Binders and Scope[slides]
11:30-12:00 Josh Ko Modularising Inductive Families[slides]
12:00-12:30 José Pedro Magalhães Formally Comparing Approaches to Datatype-generic Programming, using Agda[slides]
12:30-14:00 Lunch
Session 3
14:00-14:30 Conor McBride Crude but Effective Stratification[slides]
14:30-15:00 Duckki Oe versat: A Verified Modern SAT Solver[slides]
15:00-15:30 Brigitte Pientka Covering all Bases: Design and Implementation of a Coverage Checker for Contextual Objects
15:30-16:00 Coffee Break
Session 4
16:00-16:30 Venanzio Capretta The Polymorphic Representation of Induction-recursion[slides]
16:30-17:00 Kai Trojahner Qube: Array Programming with Dependent Types[slides]
17:00-17:30 Cezar Ionescu Dependently-typed Programming in Economic Modelling[slides] [code]
17:30-18:00 Maciej Pirog Interactive Programs in Coq, Coinductively[slides]