20 found
Sort by:
  1. Karim Nour & Khelifa Saber (2012). Some Properties of the-Calculus. 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)  
     
    My bibliography  
     
    Export citation  
  2. René David & Karim Nour (2010). Strong Normalization Results by Translation. Annals of Pure and Applied Logic 161 (9):1171-1179.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Karim Nour & Khelifa Saber (2009). A Completeness Result for the Simply Typed Λμ-Calculus. 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)  
     
    My bibliography  
     
    Export citation  
  4. Fairouz Kamareddine & Karim Nour (2007). A Completeness Result for a Realisability Semantics for an Intersection Type System. 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)  
     
    My bibliography  
     
    Export citation  
  5. Karim Nour & Khelifa Saber (2006). A Semantical Proof of the Strong Normalization Theorem for Full Propositional Classical Natural Deduction. 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.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. René David & Karim Nour (2003). A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction. 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 (8 more)  
     
    My bibliography  
     
    Export citation  
  7. Samir Farkh & Karim Nour (2003). Complete Types in an Extension of the System AF2. 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)  
     
    My bibliography  
     
    Export citation  
  8. Karim Nour & Abir Nour (2003). Propositional Mixed Logic: Its Syntax and Semantics. 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)  
     
    My bibliography  
     
    Export citation  
  9. Karim Nour (2002). Non Deterministic Classical Logic: The Λμ++ ‐Calculus. Mathematical Logic Quarterly 48 (3):357-366.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  10. Karim Nour (2002). Non Deterministic Classical Logic: The $Lambdamu^{++}$-Calculus. Mathematical Logic Quarterly 48 (3):357-366.
    In this paper, we present an extension of $lambdamu$-calculus called $lambdamu^{++}$-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.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  11. Karim Nour (2000). Mixed Logic and Storage Operators. 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 (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  12. Karim Nour (1998). S-Storage Operators. Mathematical Logic Quarterly 44 (1):99-108.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  13. Karim Nour (1997). A Conjecture on Numeral Systems. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  14. Karim Nour (1997). La Valeur d'Un Entier Classique En Lambdamu-Calcul. 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.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  15. Karim Nour (1997). La valeur dun entier classique en [mathematical formula]-calcul. Archive for Mathematical Logic 6.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  16. Karim Nour (1996). Storage Operators and ∀‐Positive Types in TTR Type System. Mathematical Logic Quarterly 42 (1):349-368.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  17. Karim Nour (1996). Storage Operators and Forall-Positive Types of System TTR. Mathematical Logic Quarterly 42: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 shown that, using Gödel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the $forall$-positive types (the universal second order quantifier appears positively in these types), and the Gödel transformations (a generalization of classical Gödel translation) of TTR type system. We generalize, by (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  18. René David & Karim Nour (1995). Storage Operators and Directed Lambda-Calculus. 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 (7 more)  
     
    My bibliography  
     
    Export citation  
  19. Karim Nour (1995). A General Type for Storage Operators. 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 (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  20. Karim Nour (1995). Strong Storage Operators and Data Types. 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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation