Verification of Functional Programs

Semester 2026-1

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: TBA, room 19-409

1.2 Official channel

1. Lecturer

2. Course coordinator

3. Course CM0858
   Sergio Ramírez Rico <mma(at)eafit(dot)edu(dot)co>
   Head of Master of Applied Mathematics

3. Course MT5010
   Andrés Sicard-Ramírez <pregrado.is(at)eafit(dot)edu(dot)co>
   Head of the undergraduate program of Computing Science.

1.3 Classes and lectures

CM0858 7097 and MT5010 7179
Tuesdays, room 17-202, 5:00 p.m. – 7:00 p.m.

1.4 Textbook

Tobias Nipkow (ed.) (2025). Functional Data Structures and Algorithms. A Proof Assistant Approach. Association for Computing (ACM). Free version.

1.5 Software

Proof assistant Isabelle.

2. Examination