Khelifa Saber
Docteur - Chercheur associé
CV
Informations diverses
- Équipe de recherche : LIMD (Logique Informatique
et Mathématiques Discrètes)
- Numéro de bureau : Bat. Chablais, Bureau 20bis
- Numéro de poste : 0033 (0) 4 79 75 87 20 poste
70 27
- E-mail : khelifa.saber@gmail.fr
Thèmes de Recherche
Lambda-calcul, Logique classique,
Réalisabilité,
Forte normalisation, Confluence, ...
Publications
1) "A
semantical proof of the strong normalization theorem for full
propositional classical natural deduction"
(sn.pdf),
[with K. Nour]
2) "Confluency
property of the call by value lambda-mu-and-or-calculus" (cbv.pdf),
[with K. Nour]
3) "A
semantic of realizability for the classical propositional natural
deduction" (rlz.pdf),
[with K. Nour]
4) "A
completeness result for the simply typed lambda-mu-calculus"
(comp.pdf)
[with K. Nour], soumis
5) "Confluence
and standardization for the lambda-mu-and-or-calculus "
(En préparation), [with K. Nour]
6) "Strong
normalization of the call by value lambda-mu-and-or-calculus"
(En préparation)
7) Thèse de doctorat "Etude d'un lambda-calcul issu
d'une logique classique" (tez.pdf)
Communications & Exposés
1) "A completeness result for the
simply typed lambda-mu-calculus" (pps.pdf).
[Workshop Computational
Interpretation of Proof], Paris, septembre 2007
2) "Etude d'un lambda-calcul issu
d'une logique classique" (slide-these.pdf).
[Thèse de doctorat], Chambéry,
Juillet 2007
3) "Introduction au lambda-mu-and-or-calculus-calcul".
[Séminaire LAIC], Clermont-Ferrand,
Novembre 2006
4) " Introduction au
lambda-calcul" (lambda.pdf).
[Séminaire LAIC], Clermont-Ferrand, Novembre 2006
5) "The Church-Rosser property for
the call by value lambda-mu-and-or-calculus"
[Ecole
Chambéry-Cracovie-Lyon], Chambéry, Juin 2005
6) "A semantic of realizability for
the lambda-mu-and-or-calculus"
[Ecole Chambéry-Cracovie-Lyon], Lyon,
Juin 2004
7) Poster " Comportement calculatoire de
quelques termes clos typés" [Ecole
Chambéry-Lyon-Turin], Aussoie,
Juin 2004
8) "Une sémantique
générale
pour la déduction naturelle classique"
[Séminaire LAMA],
Chambéry, Novembre
2003
9) "Une preuve sémantique
de la forte
normalisation du lambda-mu-and-or-calcul typé"[Séminaire
LAMA],
Chambéry, Mai 2003
10) "Confluence du
Lambda-mu-and-or-calcul" [Séminaire LAMA],
Chambéry, Décembre 2002
Enseignements
Voir CV
1) Arithmétique: AR1.dvi
, AR2.dvi
, AR3.dvi
, AR4.dvi
, AR-Exam.dvi
2) Automates et graphes: Aut0.pdf
, Aut1.pdf, Aut2.pdf, Gra1.pdf
, Gra2.pdf
, Gra-DS.pdf
3) Programmation linéaire: Proglin1.pdf
, proglin2.pdf
, proglin3.pdf
4) Mathématiques 303 : f1.dvi
, f2.pdf
, f3.pdf
, f4.pdf
, f5.pdf
, f6.pdf
, CC2-M303.pdf
, CC3-303.pdf
5) Mathématiques 204-205 : 1M204.pdf
, 2M204.pdf
, 3M204.pdf
, CC1-204.pdf
, CC2-204.pdf , CC3-204.pdf
,
1M205.pdf
, 2M205.pdf
, 3M205.pdf
, CC-205.pdf
6) Mathématiques
LSVT: SVT1.pdf
, SVT2.pdf
, SVT3.dvi
, SVT-exam.dvi
Liens utiles
* Cours de logique logique.pdf
, fonc-b.pdf,
calcul-pro.pdf
* Cours programmation
linéaire PL.df