The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
scientific article; zbMATH DE number 1565457