Locally Nameless Permutation Types

Edsko de Vries, Vasileios Koutavas

We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is…