Dependently Typed Functional Languages

Semester 2011-1

This page will be continuously updated during the course!

Course information

Lecturer

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

Lectures

Wednesdays 16:00–17:00 in room 38-524
Discussion board

Lecture material

• Slides
• Agda code: The highlighted version and the GitHub repository.

Online resources

• The Agda Wiki
  • Tutorials
  • Reference manual
  • The standard library

Some students' projects

• Andrés Eugenio Castaño-Cardenas. Using FFI’s pragmas in Agda
• Juan Pedro Villa-Isaza. Coq au vin: The Coq proof assistant and the Curry-Howard correspondence