
Initially,
due to my first adviser, Grigory Mints, I worked with simple systems of various
propositional nonclassical logics and my interest was in their applications
to category theory. (First of all, "coherence theorems".)
Categorical logics, and their prooftheoretical 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 extrarules 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 prooftheoretical
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.0801.09.1997).
Enseignement.
[Une page separée est en train d' être faite.]
J' enseigne le lambdacalcul
(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 lambdacalcul 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)