Order:
Disambiguations
Mark Bickford [3]M. Bickford [1]
  1.  17
    Innovations in computational type theory using Nuprl.S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo & E. Moran - 2006 - Journal of Applied Logic 4 (4):428-469.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  2.  17
    Connectedness of the continuum in intuitionistic mathematics.Mark Bickford - 2018 - Mathematical Logic Quarterly 64 (4-5):387-394.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  3.  48
    Intuitionistic completeness of first-order logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
    We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark