SABER KHELIFA

Khelifa Saber

Docteur - Chercheur associé

CV



Informations diverses

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.dviAR3.dviAR4.dviAR-Exam.dvi
     
      2) Automates et graphes: Aut0.pdf , Aut1.pdfAut2.pdfGra1.pdfGra2.pdfGra-DS.pdf
     
      3) Programmation linéaire: Proglin1.pdfproglin2.pdfproglin3.pdf
     
      4) Mathématiques 303 : f1.dvif2.pdf , f3.pdf , f4.pdf , f5.pdff6.pdf , CC2-M303.pdf , CC3-303.pdf
 
      5) Mathématiques 204-205 : 1M204.pdf2M204.pdf3M204.pdfCC1-204.pdf , CC2-204.pdf , CC3-204.pdf ,
          1M205.pdf2M205.pdf3M205.pdf , CC-205.pdf 

      6) Mathématiques LSVT: SVT1.pdfSVT2.pdfSVT3.dviSVT-exam.dvi

 Liens utiles

      * Cours de logique logique.pdf , fonc-b.pdf, calcul-pro.pdf

      * Cours programmation linéaire  PL.df


Retour au site du LAMA