Page perso de Karim Nour

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

Directeur du département de Mathématiques (2022-20??)

Responsable de la licence de Mathématiques (2018-2023)

Responsable ASPIR pour la licence de Mathématiques (2021-20??)

Responsable des semestres 5 et 6 de la licence de Mathématiques (2001-2022)

Responsable de l'équipe de recherche LIMD du LAMA (2007-2009)

Membre du conseil de l'UFR SFA (2002-2005)

Membre du bureau de département de mathématiques (2006-2009)

Membre du conseil du LAMA (1996-1999) et (2007-2009)

Membre de la commission de spécialistes section 25-26 (2001-20??)

Responsable des séminaires de l'équipe LIMD (2000-2002)

Responsable des prépublications du LAMA (1995-2010)

Responsable de la bibliothèque du LAMA (1995-1998)

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

Cours et TD de topologie en L3 MATH
Cours et TD d'algèbre et géométrie en L3 MATH
Cours et TD de géométrie affine et euclidienne en L3 MATH
Cours d'équations différentielles en L3 MATH
Option de logique en L3 (MATH-INFO-PHYS)
Encadrement des stages en L3 Math
Encadrement des projets de licence à l'ENS Lyon et à l'UJF Grenoble

Enseignements en M1-M2 (enseignement)

Cours et TD d'analyse pour le CAPES
Cours et TD d'algèbre linéaire et bilinéaire pour le CAPES
Cours et TD d'arithmétique et structures algébriques pour le CAPES
Préparation à l'orale pour le CAPES
Cours et TD d'ouverture mathématique pour le CAPE
Cours et TD de géométrie affine pour le CAPES et AGREG (université de la Réunion)

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, inventé vers 1930, a connu un développement important, notamment pour ses liens étroits avec les langages de programmation fonctionnelle. Ce calcul est particulièrement prisé pour sa syntaxe simple et sa capacité à exprimer toutes les fonctions calculables. Par ailleurs, le lambda-calcul typé a suscité un grand intérêt grâce au lien qu’il établit entre les programmes et les preuves en logique intuitionniste, un principe connu sous le nom de correspondance de Curry-Howard. Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et ses nombreuses extensions, ainsi que sur l'informatique théorique. Je me concentre en particulier sur les axes suivants :

L’analyse des propriétés combinatoires et du comportement algorithmique de certains termes du lambda-calcul (et ses extensions), qu’il soit pur ou typé.

L'étude de calculs issus de la logique classique, où le raisonnement par l'absurde est autorisé.

La recherche d'une définition unifiée et adéquate pour les types de données dans le lambda-calcul typé, intégrant les notions existantes.

L’approfondissement de la sémantique de réalisabilité, visant à : déterminer le comportement algorithmique de certains termes en fonction de leurs types, et établir des théorèmes de complétude, démontrant l'équivalence entre typage et réalisabilité pour certaines classes de types.

La recherche de résultats de normalisation faible et forte pour divers calculs, en utilisant la sémantique de réalisabilité ou des méthodes syntaxiques, combinatoires, arithmétiques et directes.