Switch to: References

Add citations

You must login to add citations.
  1. Towards the computational complexity of ℘Rω-terms.Karl-Heinz Niggl - 1995 - Annals of Pure and Applied Logic 75 (1-2):153-178.
    We investigate a simply typed term system ℘R ω aimed at defining partial primitive recursive functionals over arbitrary Scott domains . A hierarchy of complexity classes R n ω for functionals definable in ℘R ω is given based on a hierarchy of term classes ℘R n ωpn denoting the n th class of so-called prenormal terms . They come into play by the key observation that every term t can be transformed by what we call higher type modularization as a (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Towards the computational complexity of ℘Rω-terms.Karl-Heinz Niggl - 1995 - Annals of Pure and Applied Logic 75 (1):153-178.
    We investigate a simply typed term system ℘R ω aimed at defining partial primitive recursive functionals over arbitrary Scott domains . A hierarchy of complexity classes R n ω for functionals definable in ℘R ω is given based on a hierarchy of term classes ℘R n ωpn denoting the n th class of so-called prenormal terms . They come into play by the key observation that every term t can be transformed by what we call higher type modularization as a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Program Extraction from Normalization Proofs.Ulrich Berger, Stefan Berghofer, Pierre Letouzey & Helmut Schwichtenberg - 2006 - Studia Logica 82 (1):25-49.
    This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations