Articles


  1. Opérateurs propres de mise en mémoire. CRAS. Paris, 317, Série I, pp. 1-6, 1993.

  2. Preuve syntaxique d'un théorème de J.L. Krivine sur les opérateurs de mise en mémoire. CRAS. Paris, 318, Série I, pp. 201-204, 1994.

  3. Strong storage operators and data types. Archive for Mathematical Logic 34, pp. 65-78, 1995.

  4. Quelques résultats sur le lambda-C-calcul. CRAS. Paris, 320, Série I, pp. 259-262, 1995.

  5. Caractérisation opérationnelle des enties classiques en lambda-C-calcul. CRAS. Paris, 320, Série I, pp. 1431-1434, 1995.

  6. Entiers intuitionnistes et entiers classiques en lambda-C-calcul. Informatique Théorique et Applications, vol. 29, num 4, pp. 293-313, 1995.

  7. Storage operators and directed lambda-calculus. (with R. David). Journal of Symbolic Logic, vol 60 num 4, pp. 1054-1086, 1995.

  8. A general type for storage operators. Mathematical Logic Quarterly, vol 41, pp. 505-514, 1995.

  9. Opérateurs de mise en mémoire et types forall-positifs. Informatique Théorique et Applications, vol. 30, num 3, pp. 261-293, 1996.

  10. Storage operators and forall-positive types of system TTR. Mathematical Logic Quarterly, vol 42, pp. 349-368, 1996.

  11. An example of a non adequate numeral system. CRAS. Paris, 323, Série I, pp. 439-442, 1996.

  12. La valeur d'un entier classique en lambda-mu-calcul. Archive for Mathematical Logic 36, pp. 461-473, 1997.

  13. A syntactical proof of the operational equivalence of two lambda-terms (with R. David). Theoretical Computer Science, vol 180, pp. 371-375, 1997.

  14. A conjecture on numeral systems. Notre Dame Journal of Formal Logic, vol. 38, pp. 270-275, 1997.

  15. Une réponse négative à la conjecture de E.Tronci pour les systèmes numériques typés. Informatique Théorique et Applications, vol. 31, num 6, pp. 539-558, 1998.

  16. S-storage operators. Mathematical Logic Quarterly, vol 44, pp. 99-108, 1998.

  17. Un résultat de complétude pour les types pour-tout-positifs du système F (avec S. Farkh). CRAS. Paris, 326, Série I, pp. 275-279, 1998.

  18. Résultats de complétude pour des classes de types du système AF2 (avec S. Farkh). Informatique Théorique et Applications, vol 31, num 6, pp. 513-537, 1998.

  19. Mixed logic and storage operators. Archive for Mathematical Logic, vol 39, pp. 261-280, 2000.

  20. Les I-types du système F. Informatique Théorique et Applications, vol 35, pp. 223-237, 2001.

  21. Types de données syntaxiques du système F (avec S. Farkh). Informatique Théorique et Applications,vol 35, pp. 207-221, 2001.

  22. A non-deterministic classical logic (the lambda-mu++-calculus). Mathematical Logic Quarterly, vol 48, pp. 357 - 366, 2002.

  23. Simple proof of the completeness theorem for second order classical and intuitionictic logic by reduction to first-order mono-sorted logic (with C. Raffalli). Theoretical Computer Science, vol 308, pp. 227-237, 2003.

  24. Propositional mixed logic: its syntax and semantics (with A. Nour). Journal of Applied Non-Classical Logics, vol 13, pp. 377-390, 2003.

  25. Complete types in an extension of the system AF2 (with S. Farkh). Journal of Applied Non-Classical Logics, vol 13, pp. 73-85, 2003.

  26. A short proof of the strong normalization of classical natural deduction with disjunction (with R. David). Journal of Symbolic Logic, vol 68, num 4, pp. 1277-1288, 2003.

  27. Parametric mixed sequent calculus (with O. Laurant). Prépublication du Laboratoire de Mathématiques, num 05-05a, 2005.

  28. A semantical proof of the strong normalization theorem of full propositionnal classical natural deduction (with K. Saber). Archive for Mathematical Logic, vol 45, no 3, pp. 357-364. 2006.

  29. Arithmetical proofs of strong normalization results for symmetric lambda calculi (with R. David). Fundamenta Informaticae, vol 77, num 4, pp. 489-510, 2007.

  30. A completeness result for a realisability semantics for an intersection type system (with F. Kamareddine). Annals of Pure and Applied Logic, vol 146, pp. 180-198, 2007.

  31. A completeness result for the simply typed lambda-mu calculus (with K. Saber). Annals of Pure and Applied Logic, vol 161, pp. 109-118, 2009.

  32. Strong normalization result by translation (with R. David). Annals of Pure and Applied Logic, vol 161, pp. 1171-1179, 2010.

  33. Challenges and solutions to realisability semantics for intersection types with expansion variables (with F. Kamareddine, V. Rahli and J.B. Wells). Fundamenta Informaticae, vol 121, num 1-4, pp. 153-184, 2012.

  34. Some properties of the lambda-mu-and-or-calculus (with K. Saber). Journal of Applied Non-Classical Logics, vol 22, num 3, pp. 231-247, 2012.

  35. About range property for H (avec R. David). Logical Methods in Computer Science, vol. 10 (1:3), pp. 1-18, 2014.

  36. A revised completeness result for the simply typed lambda-mu-calculus using realizability semantics (with M. Ziadeh). Logical Methods in Computer Science, vol. 13 (3:13), pp. 1-13, 2017.

  37. Strong normalization of lambda-Sym-Prop and lambda bare-mu-mu tilde*-calculi (with P. Battyanyi) Logical Methods in Computer Science, vol. 13 (3:34), pp. 1-22, 2017.

  38. An estimation for the lengths of reduction sequences of the lambda-mu-rho-theta-calculus (with P. Battyanyi). Logical Methods in Computer Science, vol. 14 (2:17), pp. 1-35, 2018.

  39. Normalization proofs for the un-typed mu-mu'-calculus (with P. Battyanyi). AIMS Mathematics, vol. 5(4), pp. 3702-3713, 2020.

  40. Normalization properties for the simply typed lambda-mu-mu'-calculus (with P. Battyanyi). Mathematical Structures in Computer Science, vol. 32(8), pp. 1066-1098, 2022.

Proceedings


  1. On storage operators. Proceedings of a congress ``25 Years of Constructive Type Theory'' Held in Venice, 19-21 Octobre 1995, pp. 173-190, Oxford University Press 1998.

  2. A short proof of the strong normalization of the simply typed lambda-mu-calculus (with R. David). Schedae Informaticae, vol.12, pp. 27-33, 2003.

  3. Arithmetical proofs of strong normalization results for the symmetric lambda-mu-calculus (with R. David). TLCA 2005, LNCS 3461, pp. 162-178, 2005.

  4. Why the usual candidates of reducibility do not work for the symetric lambda-mu-calculus (with R. David). Electronic Notes in Theoretical Computer Science, 140, pp. 101-111, 2005.

  5. A semantics of realisability for the classical propositional natural deduction (with K. Saber). Electronic Notes in Theoretical Computer Science, 140, pp. 31-39, 2005.

  6. Classical combinatory logic. Computational Logic and Application, DMTCS proc. AF, pp. 87-96, 2006.

  7. Confluency property of the call-by-value lambda-mu-and-or-calculus (with K. Saber). Computational Logic and Application, DMTCS proc. AF, pp. 97-108, 2006.

  8. An arithmetical proof of the strong normalization for the lambda-calculus with recursive equations on types (with R. David). TLCA 2007, LNCS 4583, pp. 84-101, 2007.

  9. Realisability semantics for intersection types and expansion variables (with F. Kamareddine, V. Rahli and J.B. Wells). In ITRS'08 meeting - Turin, March 25th, 2008.

  10. A complete realisability semantics for intersection types and arbitrary expansion variables (with F. Kamareddine, V. Rahli and J.B. Wells). 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008, 1-3 September 2008, Lecture Notes in Computer Science, vol 5160, pp. 171-185, Springer-Verlag. The Marmara, Istanbul, Turkey, 2008.

En préparation


  1. Normalization properties for simply typed lambda-mu-calculus using realizability semantics (with P. Battyanyi).

  2. A second ordre typed lambda-mu-mu'-calculus (with P. Bettyanyi).

  3. Termination results for an inheritance game on trees (with A. El Zein).

  4. Parallel lambda-calculus.

Documents


  1. Opérateurs de mise en mémoire en lambda calcul pur et typé. Thèse de doctorat, université de Savoie, 1993.

  2. Programmation en lambda calcul pur et typé. Synthèse d'activités scientifiques, HDR en Mathématiques, université de Savoie, 2000.

Livres


  1. Introduction à la logique : théorie de la démonstration (cours et exercices corrigés) (avec R. David et C. Raffalli). Dunod, 2001, 2003 et 2019.

  2. Les démonstrations mathématiques (cours et exercices corrigés) (avec P. Hyvernat, R. David et C. Raffalli). Ellipse,. 2017


retour à la page de Karim Nour