Algebra and Normalisation
Scottish Programming Languages and Verification Summer School Contributed Course
Ohad Kammar 3-7 August 2026
Normalisation concerns specifying a representative in each equivalence class. It comes up whenever we want to guarantee robustness up-to the equivalence relation. For example, a normalising optimising compiler will produce the same object code when you refactor your source code using the equivalence it normalises by. Advanced type-checkers may accept or reject programs by normalising fragments of their types. Modern partial evaluators incorporate equational laws before extracting a residual program. The hallmark of modern algebra is representation theorems: characterising a structure such as the set of polynomials as the universal structure among a class of structures of interest.
In this course, we will explore the relationship between normalisation and modern algebra. We will start with algebraic expressions and universal algebra, and relate them to normalisation and partial evaluation using multi-sorted equational logic. In the second part of the course, we will turn to normalisation of open-programs through the more advanced second-order algebraic structures.
Course materials
Lectures
All lectures.
Planned structure:
Part 1: multi-sorted universal algebra
- Lecture 1
- Motivation
- Universal algebra basics: signatures & algebras
- Modern algebra: homomorphisms & representation theorems
- Lecture 2
- Modern algebra: homomorphisms & representation theorems
- Expression normalisation: free models & equational logic
- Modern partial evaluation: free extensions
- Categorical algebra basics
Part 2: second-order multi-sorted algebra * Motivation * Categories of contexts: finite product completion * Object-level and meta-level variables * Axiomatising object-level substitution * Second-order equations
Part 3: second-order normalisation(cancelled)
-
TBD
Getting help and reporting mistakes
Please never hesitate to get in touch. Approach me directly in person during the summer school or by email. You may prefer to ask a question on the #Normalisation and algebra channel on the SPLS Zulip server: spls.zulipchat.com . Others would benefit from your question in that case too!