Title: Well quasi-orders and the functional interpretation,
Abstract: The purpose of this article is to study the role of Gödel's functional
interpretation in the extraction of programs from proofs in well quasi-order
theory. The main focus is on the interpretation of Nash-Williams' famous
minimal bad sequence construction, and the exploration of a number of much
broader problems which are related to this, particularly the question of the
constructive meaning of Zorn's lemma and the notion of recursion over the
non-wellfounded lexicographic ordering on infinite sequences.