Article contents
Automorphisms of types in certain type theories and representation of finite groups
Published online by Cambridge University Press: 23 May 2018
Abstract
The automorphism groups of types in several systems of type theory are studied. It is shown that in simply typed λ-calculus λ1βη 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 λ-calculus and in Luo's framework (LF) with dependent products, any finite group may be represented.
- Type
- Paper
- Information
- Copyright
- Copyright © Cambridge University Press 2018
Footnotes
In memoriam Kosta Doen
References
- 1
- Cited by