Output details
11 - Computer Science and Informatics
Swansea University
Return to search
Output 0 of 0 in the submission
Article title
Programs from proofs using classical dependent choice
Type
D - Journal article
Title of journal
Annals of Pure and Applied Logic
Article number
-
Volume number
153
Issue number
1-3
First page of article
97
ISSN of journal
0168-0072
Year of publication
2008
URL
-
Number of additional authors
0
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
3
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-