Sergei Soloviev 

Institut de Recherche en Informatique de Toulouse (IRIT)

IRIT, porte 421 
118 route de Narbonne
31062 Toulouse cedex 4
France

Sergei.Soloviev@irit.fr 
+33 5 6155 6255 
 My picture

 


[Voir à la fin quelques pointers concernant l' enseignement.]

Research

The background (or basis, or moving force) of most of my scientific research is my interest in proof theory and its applications.
  • Initially, due to my first adviser, Grigory Mints, I worked with simple systems of various propositional non-classical logics and my interest was in their applications to category theory. (First of all, "coherence theorems".) Categorical logics, and their proof-theoretical side is a fascinating subject, it still charms me. I still work in this direction. (Since I work in categorical logics more than 30 years, for details see belov.)
  • The research taken in its history reminds a growing organism, maybe a tree. So several branches started to grow from this root (or trunk?). One of the first was the isomorphism of types - studying Cartesian Closed Categories I got interested in the notion of isomorphism of objects in a free CCC. Later a reformulation - isomorphism of types - appeared. There is a lot of activity in this direction nowadays.
  • Next important branch was the study of the second order propositional calculi. This work was due to my collaboration with Guiseppe Longo - one of the happiest periods of my life as a researcher. We studied "system F" with some extra-rules for term equality. In particular we obtained a genericity theorem for the system with so called "axiom C", and later studied coercive subtyping in this system.
  • Subtyping begot (another kind of) subtyping. At University of Durham (my previous place of work - also a very good period) I've been involved in the project "Subtyping, Inheritance and Reuse: Developing Expressive Type Theory for Formal Analysis" (more about coercive subtyping for dependent types you may find at the page Zhaohui Luo ). More specifically, we worked on a general theory of Coercive Subtyping for dependent type systems (Luo's LF, UTT). See also the following papers:

    • [1] Z. Luo. Coercive subtyping in type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997. [dvi
    and psfiles available.]

    [2] A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. Proc. of TYPES'96. [ps file available.]

    An interesting link may be to the home page of Types WG Workshop on Subtyping, Inheritance, and Modularisation of Proofs (Durham, 30.08-01.09.1997).

    Enseignement. [Une page separée est en train d' être faite.]

    J' enseigne le lambda-calcul (DEA),  les mathèmatiques discrètes (IUP), logique modale et temporelle (DESS), ainsi que
    les probabilités pour l'informatique (licence).

    (DEA) 
    Voici un  lien à un texte de support (l'introduction au lambda-calcul typé).

      (un fichier ps.gz)

    et une autre lien (solutions de l'exam 2000)

     (un fichier ps.gz) 

    (LICENCE)

    Voici un lien:

    (un fichier ps.gz)

 
Last modified: Mon Feb 26 11:06:09 CET 2001