Program extraction from nominal proofs

So far there is quite a bit of classical reasoning involved in the
nominal approach, most prominently in the choice of fresh atoms and
in the construction of functions over alpha-equivalence classes. It
would be nice to have a version of the nominal approach that is a
bit friendlier to the extraction-of-programs from proof movement

Christian Urban