This module gives a high-level introduction to the relational theory of reduction systems. The first part of the module focuses on the so-called mathematics of syntax and covers the basic mathematical analysis of abstract syntax. Building upon that, the second part of the module introduces relational notions of reduction on syntax-based systems.
Introduction (Relational reasoning in operational semantics; relational operationalism)
Basic calculus of relations and relational modelling of abstract reduction systems (minimal notions only)
Introduction to the Mathematics of Syntax (first-order case only)
Signature functors
Syntax as free algebras
Structural induction and recursion
Monads and substitutions
Syntax-based Relational Rewriting
Relators
Substitution and Compatibility
Parallel Reduction
Confluence of Orthogonal Systems (time permitting)
Slides by Marcelo Fiore on Abstract Syntax and Substitution (up to variable sets, excluded)
An Introduction to Category Theory for (second-order) Syntax Modelling, by R.L Crole (final version here)
Abstract Syntax and Variable Binding (advanced paper)
Program Design by Calculation (part II gives a good introduction to relational reasoning)
A Calculational Approach to Mathematical Induction (advanced paper on relational reasoning)