Switch to: References

Add citations

You must login to add citations.
  1. A semantical storage operator theorem for all types.Christophe Raffalli - 1998 - Annals of Pure and Applied Logic 91 (1):17-31.
    Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivine's storage operator theorem shows that any term of type ¬D → ¬D*, where D* is the Gödel translation of D, is a storage operator for the terms of type D when D is a data-type or a formula with only positive second order quantifiers. We prove that a new semantical version of Krivine's theorem is valid for every types. This also gives a simpler proof (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Complete Types in an Extension of the System AF2.Samir Farkh & Karim Nour - 2003 - Journal of Applied Non-Classical Logics 13 (1):73-85.
    In this paper, we extend the system AF2 in order to have the subject reduction for the $betaeta$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.
    Download  
     
    Export citation  
     
    Bookmark