Sciweavers

Share
CIE
2006
Springer

Understanding and Using Spector's Bar Recursive Interpretation of Classical Analysis

9 years 11 months ago
Understanding and Using Spector's Bar Recursive Interpretation of Classical Analysis
This note reexamines Spector's remarkable computational interpretation of full classical analysis. Spector's interpretation makes use of a rather abstruse recursion schema, so-called bar recursion, used to interpret the double negation shift DNS. In this note bar recursion is presented as a generalisation of a simpler primitive recursive functional needed for the interpretation of a finite (intuitionistic) version of DNS. I will also present two concrete applications of bar recursion in the extraction of programs from proofs of -theorems in classical analysis.
Paulo Oliva
Related Content
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CIE
Authors Paulo Oliva
Comments (0)
books