KARIM NOUR
Maître de conférences : hors classe - échelon exceptionnel, (HDR)
à l'université Savoie Mont Blanc
Informations diverses
- Laboratoire : LAMA (LAboratoire de MAthématiques)
- Equipe de recherche : LIMD (Logique, Informatique et Mathématiques Discrètes)
- Numéro de bureau : 127
- Numéro de poste : 8627
- Adresse : Université Savoie Mont Blanc, Bâtiment Le Chablais, Rue du lac de la Thuile, Campus Scientifique, 73376 Le Bourget-du-Lac Cedex, France
- tel : +33 4 79 75 86 27
- fax : +33 4 79 75 81 42
- Email : karim.nour@univ-smb.fr
Diplômes
- Habilitation à diriger des recherches en Mathématiques, "Programmation en lambda-calcul pur et typé", Université Savoie Mont Blanc, janvier 2000
- Jury : J.-L. Krivine, R. David, H. Barendregt, J.-Y. Girard, S. Ronchi.
- Doctorat en Mathématiques, "Opérateurs de mise en mémoire en lambda-calcul pur et typé", Université Savoie Mont Blanc, janvier 1993
- Jury : J.-L. Krivine, R. David, C. Paulin, J.-Y. Girard, S. Ronchi, T. Ehrhard.
- DEA de Mathématiques pures, Université Claude Bernard - Lyon I, 1990
- Projet : étude d'un article de J.-L. Krivine sur les Opérateurs de mise en mémoire des entiers de Church.
- Maitrise de Mathématiques pures, Université Libanaise - Faculté des sciences (section III), 1988
Responsabilités
Enseignements
- Enseignements en L1
- Cours et TD "Logique et ensembles" en L1
- TD d'algèbre linéaire en L1
- TD de probabilités et statistiques en L1
- Enseignements en L2
- Cours et TD d'algèbre (Espaces Euclidiens) en L2
- TD de Mathématiques (analyse et algèbre) en L2
- Cours et TD de Mathématiques en L2 STAPS
- TD de Mathématiques en L2 PEIP
- Enseignements en L3
- Enseignements en M1 (enseignement)
- Enseignements en M1-M2 (recherche)
- Encadrement des stages en M1 Math
- Encadrement des projets de magistère à l'ENS Lyon et à l'UJF Grenoble
- Cours de logique et lambda-calcul en M2 Recherche
Axes de recherche
Le lambda-calcul pur a été inventé vers 1930, et a connu un développement considérable pour ses rapports étroits avec les langages de programmation fonctionnelle.
L'intérèt principal de ce calcul provient essentiellement de la simplicité de sa syntaxe et de sa capacité à programmer toutes les fonctions calculables.
Le lambda-calcul typé suscite aussi un grand intérèt à cause du lien qu'il établit entre les notions de programme et de preuve en logique intuitionniste,
c'est ce qu'on appelle la "correspondance de Curry-Howard".
Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul avec ses multiples extensions
et l'informatique théorique. Je m'intéresse tout spécialement aux thèmes suivants :
- L'étude des propriétés combinatoires et le comportement algorithmique de quelques termes du lambda-calcul pur et typé.
- L'étude de quelques calculs issus de la logique classique où le raisonnement par l'absurde est autorisé.
- La recherche d'une définition adéquate (reliant tout ce qui existe actuellement) pour les types de données en lambda-calcul typé.
- L'approfondissement de l'étude de la sémantique de réalisabilité pour, d'un part, trouver le comportement
algorithmique de quelques termes à partir de leurs types et, d'autre part, prouver des théorèmes de complétude
(équivalence entre typage et réalisabilité) pour des classes de types.
- La recherche des résultats de faible et forte normalisation pour différents calculs soit en passant par une sémantique
de réalisabilité soit en utilisant des méthodes syntaxiques, combinatoires, arithmétiques et directes.
- La terminaison (faible et forte) d'un processus d'héritage sur des arbres.
Publications
Exposés dans des congrés, séminaires, groupes de travail,...
Thèses encadrées
Activité associative
- Fondateur et directeur de l'école AstRolABE de CICH depuis 2001.
- L'école accueille 220 enfants de 5 à 16 ans pour leur enseigner la langue et la culture arabes.
- L'équipe pédagogique de l'école est composée de 32 enseignants bénévoles.