Automorphisms of types in certain type theories and representation of finite groups

摘要

The automorphism groups of types in several systems of type theory are studied. It is shown that in simply typed lambda-calculus lambda(1)beta eta and in its extension with surjective pairing and terminal object these groups correspond exactly to the groups of automorphisms of finite trees. In second-order lambda-calculus and in Luo's framework (LF) with dependent products, any finite group may be represented.