Peter Dybjer (Chalmers University of Technology) has been invited to the University of Oslo to give an introduction to Agda.

Dybjer is a fellow on Homotopy Type Theory and Univalent Foundations at CAS.

Abstract: Agda is a functional language with dependent types which has been developed by the Programming Logic Group in Göteborg. It is based on Martin-Löf’s intuitionistic type theory, but adds numerous programming language features to it. I will give an introduction to Agda by showing some examples of how to write programs and proofs in it.

You can read more on the Agda wiki.