- Tools for modular syntax with binders
- Introductory example: counting funtions
- Case study 1: Modular Type-Safety Proofs (originally in Agda)
- Case Study 2: Monotonicty and Type Safety for big-step mini-ML
- Autosubst 2 generated code
- mini-ML: lambda expression
- mini-ML: boolean expressions
- mini-ML: arithmetic expressions
- mini-ML: natCase expressions
- mini-ML: recursive abstractions
- Autosubst 2 generated combined mini-ML types
- Autosubst 2 generated combined mini-ML types without fix
- Composed results for mini-ML
- Composed results for mini-ML witout fix
- Case study 3: Type preservation, weak head normalisation and strong normalisation for mini-ML