Switch to: Citations

Add references

You must login to add references.
  1. Games with 1-backtracking.Stefano Berardi, Thierry Coquand & Susumu Hayashi - 2010 - Annals of Pure and Applied Logic 161 (10):1254-1269.
    We associate with any game G another game, which is a variant of it, and which we call . Winning strategies for have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over , and vice versa. Through we can express in algorithmic form, as a recursive winning strategy, many common proofs of non-constructive Mathematics, namely exactly the theorems of the (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • A semantics of evidence for classical arithmetic.Thierry Coquand - 1995 - Journal of Symbolic Logic 60 (1):325-337.
    Download  
     
    Export citation  
     
    Bookmark   22 citations  
  • Interpretation of analysis by means of constructive functionals of finite types.Georg Kreisel - 1959 - In A. Heyting (ed.), Constructivity in mathematics. Amsterdam,: North-Holland Pub. Co.. pp. 101--128.
    Download  
     
    Export citation  
     
    Bookmark   55 citations  
  • On the interpretation of intuitionistic number theory.S. C. Kleene - 1945 - Journal of Symbolic Logic 10 (4):109-124.
    Download  
     
    Export citation  
     
    Bookmark   79 citations  
  • A constructive analysis of learning in Peano Arithmetic.Federico Aschieri - 2012 - Annals of Pure and Applied Logic 163 (11):1448-1470.
    We give a constructive analysis of learning as it arises in various computational interpretations of classical Peano Arithmetic, such as Aschieri and Berardi learning based realizability, Avigad’s update procedures and epsilon substitution method. In particular, we show how to compute in Gödel’s system T upper bounds on the length of learning processes, which are themselves represented in T through learning based realizability. The result is achieved by the introduction of a new non standard model of Gödel’s T, whose new basic (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations