You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Birmingham » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Birmingham

Return to search Previous output Next output

Output 44 of 157 in the submission

Output title

Computational Interpretations of Analysis via Products of Selection Functions

Type

E - Conference contribution

DOI

10.1007/978-3-642-13962-8_16

Name of conference/published proceedings

Programs, Proofs, Processes : 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30 – July 4, 2010. Proceedings

Volume number

6158

Issue number

First page of article

141

ISSN of proceedings

0302-9743

Year of publication

2010

URL

Number of additional authors

Additional information

<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.

Interdisciplinary

Cross-referral requested

Research group

G - Theory of Computation

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract