Output details
11 - Computer Science and Informatics
University of Birmingham
Computational Interpretations of Analysis via Products of Selection Functions
<11>We show that the computational interpretation of full comprehension via two well-known functional interpretations (dialectica and modified realizability) corresponds to two closely related infinite products of selection functions (a certain Tychonoff program previously developed by Escardo, and a modification tailored to account for the dialectica interpretation). This has applications to proof mining, ranging from program extraction from classical proofs, to the mere extraction of bounds where they are previously unknown. A proof-of-concept example (no injection from the Baire space to the natural numbers) was developed for invited tutorials at conferences, and implemented in the functional programming language Haskell.