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

Output details

11 - Computer Science and Informatics

Swansea University

Return to search Previous output Next output

Output 0 of 0 in the submission

Article title

Programs from proofs using classical dependent choice

Type

D - Journal article

DOI

10.1016/j.apal.2008.01.004

Title of journal

Annals of Pure and Applied Logic

Article number

Volume number

153

Issue number

1-3

First page of article

ISSN of journal

0168-0072

Year of publication

2008

URL

Number of additional authors

Additional information

<11> This is the first article about program extraction from proofs based upon classical choice principles that are formalised in a theorem prover. The case study in this article was taken up and implemented by Martin Escardo (Birmingham) and Paulo Oliva (Queen Mary) in Agda (http://www.cs.bham.ac.uk/~mhe/pigeon). It started a collaboration between Swansea, Birmingham, and Queen Mary on the comparison of modified bar recursion and selection functions as realizers for choice principles.

Interdisciplinary

Cross-referral requested

Research group

A - Theoretical Computer Science

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract