Switch to: Citations

Add references

You must login to add references.
  1. Provably total functions of intuitionistic bounded arithmetic.Victor Harnik - 1992 - Journal of Symbolic Logic 57 (2):466-477.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
    Download  
     
    Export citation  
     
    Bookmark   131 citations  
  • Functional interpretations of feasibly constructive arithmetic.Stephen Cook & Alasdair Urquhart - 1993 - Annals of Pure and Applied Logic 63 (2):103-200.
    A notion of feasible function of finite type based on the typed lambda calculus is introduced which generalizes the familiar type 1 polynomial-time functions. An intuitionistic theory IPVω is presented for reasoning about these functions. Interpretations for IPVω are developed both in the style of Kreisel's modified realizability and Gödel's Dialectica interpretation. Applications include alternative proofs for Buss's results concerning the classical first-order system S12 and its intuitionistic counterpart IS12 as well as proofs of some of Buss's conjectures concerning IS12, (...)
    Download  
     
    Export citation  
     
    Bookmark   33 citations