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.)
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.
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
Inheritance and Reuse: Developing Expressive Type Theory for Formal Analysis"
(more about coercive subtyping for dependent types you may find at the page
we worked on a general theory of Coercive Subtyping for dependent type systems
(Luo's LF, UTT). See also the
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
A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical
aspects of coercive subtyping. Proc. of TYPES'96. [ps
interesting link may be to the home page of
WG Workshop on Subtyping, Inheritance, and Modularisation of Proofs
[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
pour l'informatique (licence).
Voici un lien
à un texte de support (l'introduction au lambda-calcul typé).
et une autre lien (solutions de l'exam 2000)
Voici un lien: