KARIM NOUR
Maître de conférences (HDR)
à l'université de Savoie Mont Blanc
Informations diverses
- 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
Maitrise de Mathématiques pures, Université Libanaise -
Faculté des sciences (section III), 1988
Responsabilités
Enseignements
- Enseignements 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 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.
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 200 enfants de 5 à 16 ans pour leur enseigner la
langue et la culture arabes.
- L'équipe pédagogique de l'école est formée de 25 enseignants
bénévoles.