CM0859 Type Theory

Semester 2017-1

This page will be continuously updated during the course!

Course Information

Lecturer

Andreas Abel
Department of Computer Science and Engineering. Chalmers University of Technology, Gothenburg, Sweden

Andrés Sicard Ramírez <asr(at)eafit(dot)edu(dot)co>

Lectures

Group 001, 17:00–19:00, classroom 38-525

Course Material

Slides, references, code, etc.

Additional Agda Online resources

• The Agda Wiki
• Tutorials
  • Ulf Norell and James Chapman. Dependently Typed Programming in Agda. This is aimed at functional programmers.
  • Ana Bove and Peter Dybjer. Dependent Types at Work. A gentle introduction including logic and proofs of programs.
  • Other tutorials
• User Manual