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]