This is the page for the ISR 2017 advanced track course on commutation.

• slides
     VvO    JN (handout version)
• some example rewrite systems used during the lecture
     addsub.trs    opt1.trs    opt2.trs    bool.trs    opt3.trs    mapmap.trs    foldrsum.trs
• Isabelle – in case you can't get enough of formalizing you can try to prove that strong commutation implies commutation in Isabelle using the following skeleton theory:
     Commutation_Ex.thy    here's a possible solution: Commutation_Sol.thy