Abstract de la publi numéro 19117

The notion of automorphism of types is defined, as usual, it is an isomorphism A->A. The groups of automorphisms of types in different type theories are studied. It is shown that in simply typed lambda calculus the automorphism groups of types are exactly the groups of automorphisms of finite trees. In second-order lambda calculus (system F) and in case of dependent product types any finite group can be represented.