Slides presented at AIM9
Shin-Cheng Mu (Academia Sinica) Algebra of Programming using Dependent Type
Nils Anders Danielsson (The University of Nottingham) An ad-hoc and monolithic method for ensuring that corecursive definitions are productive Attach:nad.pdf
Anton Setzer (Swansea University) Coalgebras in Dependent Type Theory Attach:setzer.pdf
Yoshinori Tanabe (The University of Tokyo) Verification of the Deutsch-Schorr-Waite marking algorithm on Agda
Yoshifumi Yuasa (Tokyo Institute of Technology) A case study in automotive engineering : Verifying electric control units with Agda.
Conor McBride(University of Strathclyde) Definitional Equality and Neutral Terms
Norio Kato (AIST) Features required for an interactive verification environment
Bengt Nordstrom (Chalmers University of Technology) Towards a basis for human-computer dialogue
Peter Dybjer (Chalmers University of Technology) Secret thoughts about Martin-Löf's meaning explanations
Andreas Abel (Ludwig-Maximilians-University Munich) Sized Types in Agda