Switch to: References

Add citations

You must login to add citations.
  1. Constructive Validity of a Generalized Kreisel–Putnam Rule.Ivo Pezlar - forthcoming - Studia Logica.
    In this paper, we propose a computational interpretation of the generalized Kreisel–Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry–Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • 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 (...)
    Download  
     
    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.
    Download  
     
    Export citation  
     
    Bookmark   5 citations