Here is the support material for the course series I am giving at CMI during January 2017.
Well-quasi-orderings (WQOs) are a fundamental tool in logic and computer science. They provide termination arguments in a large number of decidability (or finiteness, regularity, ...) results. In constraint solving, automated deduction, program analysis, and many more fields, wqos usually appear under the guise of specific tools, like Dickson's Lemma (for tuples of integers), Higman's Lemma (for words and their subwords), Kruskal's Tree Theorem and its variants (for finite trees with embeddings), and recently the Robertson-Seymour Theorem (for graphs and their minors). What is not very well known is how to analyze the complexity of wqo-based algorithms.
The purpose of this course is to provide an introduction to the algorithmic aspects of wqos: to present generic algorithms working on large classes of problems, to introduce the techniques used to prove complexity upper bounds and lower bounds, to explain the use of wqo ideals in algorithms. The presentation is largely based on recent courses prepared and given in collaboration with Sylvain Schmitz (LSV).
They are available here.