PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

Gilles Dowek, Murdoch J. Gabbay

Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In P…