Articles publiés

  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. 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.
  28. Arithmetical proofs of strong normalization results for symmetric lambda calculi (with R. David). Fundamenta Informaticae, vol 77, num 4, pp. 489-510, 2007.
  29. 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.
  30. 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.
  31. Strong normalization result by translation (with R. David). Annals of Pure and Applied Logic, vol 161, pp. 1171-1179, 2010.
  32. Challenges and solutions to realisability semantics for intersection types with expansion variables (with F. Kamareddine, V. Rahli and J.B. Wells). A paraître dans Fundamenta Informaticae, 2012.
  33. Some properties of the lambda-mu-and-or-calculus (with K. Saber). A paraître dans Journal of Applied Non-Classical Logics, 2012.

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. A complete realisability semantics for intersection types and expansion variables (with F. Kamareddine, V. Rahli and J.B. Wells). Accepté dans le workshop 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 volume 5160/2008, pp. 171-185, Springer-Verlag. The Marmara, Istanbul, Turkey.

Livres

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

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, 2000.

Rapports internes

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

Articles soumis

  1. About range property for H. (avec R. David)

Articles en préparation

  1. A second order parallel lambda-calculus.
  2. A completeness result for the second order typed lambda-mu calculus. (avec M. Ziadeh)

retour à la page de Karim Nour