Slides Presented At AIM 9

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