Reading group on Certified Programming with Dependent Types. All meetings take place from 13:30 to 14:30. All participants read the chapter in advance. When there is a streams seminar we cancel the reading group. Now that we've worked our way through CPDT, we'll spend a few weeks studying Agda. Wouter offers to discuss other papers from the extensive list of agda papers.