Switch to: References

Add citations

You must login to add citations.
  1. Parameter-free polymorphic types.Klaus Aehlig - 2008 - Annals of Pure and Applied Logic 156 (1):3-12.
    Consider the following restriction of the polymorphically typed lambda calculus . All quantifications are parameter free. In other words, in every universal type α.τ, the quantified variable α is the only free variable in the scope τ of the quantification. This fragment can be locally proven terminating in a system of intuitionistic second-order arithmetic known to have strength of finitely iterated inductive definitions.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • A Buchholz Rule for Modal Fixed Point Logics.Gerhard Jäger & Thomas Studer - 2011 - Logica Universalis 5 (1):1-19.
    Buchholz’s Ω μ+1-rules provide a major tool for the proof-theoretic analysis of arithmetical inductive definitions. The aim of this paper is to put this approach into the new context of modal fixed point logic. We introduce a deductive system based on an Ω-rule tailored for modal fixed point logic and develop the basic techniques for establishing soundness and completeness of the corresponding system. In the concluding section we prove a cut elimination and collapsing result similar to that of Buchholz (Iterated (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations