Logic and Functional Programming

Heidelberg University, Summer Semester 2026

A drawing showing an illustration of the elimination rule for the existential quantifier, where the space of points x satisfying a given predicate P is represented as a Sigma-type, and the input f from which one can deduce a given proposition Q from the existence of an x with property P(x), which is is a dependent function sending x to a proof that P(x) implies Q, is shown as a function from the fibre above x to Q.

The elimination rule for the existential quantifier

Overview

Martin-Löf’s type theory provides a common foundation for mathematics, logic and functional programming. In this course, we give an account of the basics of type theory with a view towards applications in mathematics. The course will combine a theoretical exposition of the concepts with their implementation in a proof assistant.

  • Target audience: Bachelor students of mathematics or computer science.
  • Instructor: Florent Schaffhauser.
  • Language of instruction: English.
  • Pre-registration on Müsli (to estimate the number of participants).

Syllabus

  • Types and terms. Judgments and contexts.
  • Inference rules. Natural deduction.
  • Propositional calculus. Decidability.
  • Axioms. Models. Soundness.
  • Inductive types. Recursion. Pattern matching.
  • Type families. Dependent pairs.
  • Dependent function types. Induction.
  • Propositions as types. Predicates. Subtypes.
  • Relations. Ordered structures.
  • Identity types. Sets.
  • Number systems. Elementary arithmetic.
  • Algebraic data types.
  • Type equivalences.
  • Propositional truncation. Principle of unique choice.

Proof assistants

As a means to experiment with the logic and explore formal proofs of mathematical statements, students will be taught to use a proof assistant. At the end of the course, they will have developed an understanding of the type theory and logic underpinning modern proof assistants and acquired basic programming skills related to the formalisation of mathematics and software verification.

From Stdlib Require Import Utf8.

Theorem exists_elim (X : Set) (P : X → Prop) (Q : Prop) : (∀ x : X, P x → Q) ∧ (∃ x : X, P x) → Q.
Proof.
  intro term.
  destruct term as [f [x proof]].
  apply (f x).
  exact proof.
Qed.

Check exists_elim.
Print exists_elim.

Tentative schedule

  • Lectures: 4h per week. Tuesday-Thursday 14:00-16:00.
  • Exercises: 2h per week. Monday 16:00-18:00.

Prerequisites

There are no formal prerequisites for this course but familiarity with abstract reasoning and algebraic structures might be helpful.

Evaluation

The course is completed with a graded oral or written exam. To be admitted to the exam, students will need to collect at least 50% of the points from the graded problem sets. The final grade is determined by the grade of the exam. The requirements for the assignment of credits follows the regulations in section modalities for examinations.