Switch to: Citations

Add references

You must login to add references.
  1. Constructive mathematics in theory and programming practice.Douglas Bridges & Steeve Reeves - 1999 - Philosophia Mathematica 7 (1):65-104.
    The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Recherches Sur la Th”Eorie de la D”Emonstration.J. Herbrand - 1930 - Dissertation, Universit’e de Paris
    Download  
     
    Export citation  
     
    Bookmark   34 citations  
  • (1 other version)Interpreting classical theories in constructive ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
    A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • Was Sind und was Sollen Die Zahlen?Richard Dedekind - 1888 - Cambridge University Press.
    This influential 1888 publication explained the real numbers, and their construction and properties, from first principles.
    Download  
     
    Export citation  
     
    Bookmark   182 citations  
  • Weak theories of nonstandard arithmetic and analysis.Jeremy Avigad - manuscript
    A general method of interpreting weak higher-type theories of nonstandard arithmetic in their standard counterparts is presented. In particular, this provides natural nonstandard conservative extensions of primitive recursive arithmetic, elementary recursive arithmetic, and polynomial-time computable arithmetic. A means of formalizing basic real analysis in such theories is sketched.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • (1 other version)Types in Logic, Mathematics and Programming.Robert L. Constable - 2000 - Bulletin of Symbolic Logic 6 (4):476-477.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • (1 other version)Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
    A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.
    Download  
     
    Export citation  
     
    Bookmark   12 citations