@inproceedings{80edc7404ab046f09ab377f518229d9e,
title = "Applying G{\"o}del's Dialectica interpretation to obtain a constructive proof of Higman's lemma",
abstract = "We use G{\"o}del's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive {"}minimal bad sequence{"} proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words.",
author = "Thomas Powell",
year = "2012",
doi = "10.4204/EPTCS.97",
language = "English",
volume = "97",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "Open Publishing Association",
pages = "49--62",
booktitle = "Proceedings Fourth Workshop on Classical Logic and Computation",
}