17 found
Order:
  1.  72
    A short proof of the strong normalization of classical natural deduction with disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
    We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  2. A semantical proof of the strong normalization theorem for full propositional classical natural deduction.Karim Nour & Khelifa Saber - 2006 - Archive for Mathematical Logic 45 (3):357-364.
    We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  3.  91
    Mixed logic and storage operators.Karim Nour - 2000 - Archive for Mathematical Logic 39 (4):261-280.
    In 1990 J-L. Krivine introduced the notion of storage operators. They are $\lambda$ -terms which simulate call-by-value in the call-by-name strategy and they can be used in order to modelize assignment instructions. J-L. Krivine has shown that there is a very simple second order type in AF2 type system for storage operators using Gödel translation of classical to intuitionistic logic. In order to modelize the control operators, J-L. Krivine has extended the system AF2 to the classical logic. In his system (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  4.  25
    A General Type for Storage Operators.Karim Nour - 1995 - Mathematical Logic Quarterly 41 (4):505-514.
    In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $lambda$-calculus, the 'call by value' in a context of a 'call by name'. J.L. Krivine has shown that, using Gödel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of this (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  30
    (1 other version)Storage Operators and ∀‐positive Types in TTR Type System.Karim Nour - 1996 - Mathematical Logic Quarterly 42 (1):349-368.
    In 1990, J. L. Krivine introduced the notion of storage operator to simulate “call by value” in the “call by name” strategy. J. L. Krivine has showed that, using Gödel translation of classical into intuitionistic logic, one can find a simple type for the storage operators in AF2 type system. This paper studies the ∀-positive types and the Gödel transformations of TTR type system. We generalize by using syntactical methods Krivine's theorem about these types and for these transformations. We give (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  26
    Strong storage operators and data types.Karim Nour - 1995 - Archive for Mathematical Logic 34 (1):65-78.
    The storage operators were introduced by J.L. Krivine ([6]); they are closed λ-terms which, for some fixed data type (the integers for example), allow to simulate “call by value” while using “call by name”. J.L. Krivine showed that such operators can be typed, in the type system, using Gödel's translation from classical to intuitionistic logic ([8]).This paper studies the existence of storage operators which give a normal form as result (strong storage operators) for recursive and iterative representation of data in (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7. Storage operators and directed lambda-calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
    Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability of the set (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  8.  34
    Strong normalization results by translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.
    We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  9.  57
    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.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  10.  18
    A completeness result for a realisability semantics for an intersection type system.Fairouz Kamareddine & Karim Nour - 2007 - Annals of Pure and Applied Logic 146 (2):180-198.
    In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11.  35
    A Conjecture on Numeral Systems.Karim Nour - 1997 - Notre Dame Journal of Formal Logic 38 (2):270-275.
    A numeral system is an infinite sequence of different closed normal -terms intended to code the integers in -calculus. Barendregt has shown that if we can represent, for a numeral system, the functions Successor, Predecessor, and Zero Test, then all total recursive functions can be represented. In this paper we prove the independancy of these three particular functions. We give at the end a conjecture on the number of unary functions necessary to represent all total recursive functions.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  12.  24
    A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
    In this paper, we define a realizability semantics for the simply typed $lambdamu$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  41
    (2 other versions)La valeur d'un entier classique en $\lambda\mu$ -calcul.Karim Nour - 1997 - Archive for Mathematical Logic 36 (6):461-473.
    In this paper, we present three methods to give the value of a classical integer in $\lambda\mu$ -calculus. The first method is an external method and gives the value and the false part of a normal classical integer. The second method uses a new reduction rule and gives as result the corresponding Church integer. The third method is the M. Parigot's method which uses the J.L. Krivine's storage operators.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  13
    (1 other version)Non Deterministic Classical Logic: The -calculus.Karim Nour - 2002 - Mathematical Logic Quarterly 48 (3):357-366.
    In this paper, we present an extension of λμ-calculus called λμ++-calculus which has the following properties: subject reduction, strong normalization, unicity of the representation of data and thus confluence only on data types. This calculus allows also to program the parallel-or.
    Direct download  
     
    Export citation  
     
    Bookmark  
  15.  43
    Propositional Mixed Logic: Its Syntax and Semantics.Karim Nour & Abir Nour - 2003 - Journal of Applied Non-Classical Logics 13 (3-4):377-390.
    In this paper, we present a propositional logic (called mixed logic) containing disjoint copies of minimal, intuitionistic and classical logics. We prove a completeness theorem for this logic with respect to a Kripke semantics. We establish some relations between mixed logic and minimal, intuitionistic and classical logics. We present at the end a sequent calculus version for this logic.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16.  22
    S-Storage Operators.Karim Nour - 1998 - Mathematical Logic Quarterly 44 (1):99-108.
    In 1990, J. L. Krivine introduced the notion of storage operator to simulate, for Church integers, the “call by value” in a context of a “call by name” strategy. In the present paper we define for every λ-term S which realizes the successor function on Church integers the notion of S-storage operator. We prove that every storage operator is an S-storage operator. But the converse is not always true.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  17.  30
    Some properties of the -calculus.Karim Nour & Khelifa Saber - 2012 - Journal of Applied Non-Classical Logics 22 (3):231-247.
    In this paper, we present the -calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church–Rosser property of this system is proved using the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark