Swapping: a natural bridge between named and indexed explicit substitution calculi
Uncurrying for Innermost Termination and Derivational Complexity
Standardisation for constructor based pattern calculi
Higher-order Rewriting for Executable Compiler Specifications
On the Implementation of Dynamic Patterns
A Calculus of Coercions Proving the Strong Normalization of MLF
Equivalence of algebraic λ-calculi