@inbook{21e1d8cc3e854d0293fd4398970b1661,
title = "Well quasi-orders and the functional interpretation",
abstract = "The purpose of this article is to study the role of G{\"o}del{\textquoteright}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{\textquoteright} 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{\textquoteright}s lemma and the notion of recursion over the non-wellfounded lexicographic ordering on infinite sequences.",
author = "Thomas Powell",
year = "2020",
doi = "10.1007/978-3-030-30229-0_9",
language = "English",
series = "Trends in Logic",
publisher = "Springer International Publishing",
pages = "221--269",
editor = "Schuster, {Peter } and Monika Seisenberger and Andreas Weiermann",
booktitle = "Well-Quasi Orders in Computation, Logic, Language and Reasoning",
address = "Switzerland",
}