CM0859 – MT5009 Type Theory

Semester 2025-2

This page will be continuously updated during the course!

1. Course Information

1.1 Lecturer

Andrés Sicard-Ramírez asr(at)eafit(dot)edu(dot)co
Office hours: Tuesdays, 2:30 p.m. – 3:30 p.m., room 19-409

1.2 Official channel

  1. Lecturer

  2. Course coordinator

  3. CM0859: Head of Master of Applied Mathematics
    Sergio Ramírez Rico <ssramirezr(at)eafit(dot)edu(dot)co>

  4. MT5009: Head of the undergraduate program of Computing Science
    Andrés Sicard-Ramírez asr(at)eafit(dot)edu(dot)co

1.3 Lectures

CM0859 Class 7481 and MT5009 Class 8122
Wednesdays, room 07-101, 5:00 p.m. – 7:00 p.m.

2. Examination

2.1 Percentages

Activity %
Two exams 25% each
Two programming labs 15% each
Homeworks 20%

2.2 Dates and descriptions

Activity Week Date/Dealine Description/Textbook material
Exam 1 10th Wednesday, September 17 TBA
Programming Lab 1 13th Friday, October 17, 11:59 p.m. Proof Assistants
Programming Lab 2 TBA TBA TBA
Exam 2 17th Wednesday, November 12 TBA

3. Slides

Subject Slides
Course Introduction [ pdf ]
Constructivism [ pdf ]
Natural Deduction [ pdf ]
Typed Lambda Calculus (or Proof as Programs) [ pdf ]
Martin-Löf Type Theory [ pdf ]
Dependent Types in Agda N/A
Appendix: Testing with QuickCheck [ pdf ]
Appendix: Computer Assisted Proofs [ pdf ]