The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

Apologies for chiming in slightly late, but:

> Another reference (but, again, not really a package) is Nominal Reasoning Techniques in Coq by Brian Aydemir, Aaron 
> Bohannon, Stephanie Weirich (https://www.seas.upenn.edu/~sweirich/papers/nominal-coq/lfmtp06.pdf)
> But this is more like an axiomatic approach to defining a nominal "interface" to your syntax and then justifying this 
> interface by using locally nameless representation. So, again, no automatic generation of alpha conversion.

Regarding Stephanie Weirich, when two years ago an analogous subject came up on this list [1] there were pointers to her 
newer stuff:

https://github.com/DeepSpec/dsss17/tree/master/Stlc

https://www.youtube.com/watch?v=zBCP20jGE54

https://www.youtube.com/watch?v=Xo8MzrH4aj0

Other things mentioned in that thread might be also helpful.

[1] https://coq-club.inria.narkive.com/T7HMhwa8/nominal-reasoning-in-coq

********

> I am not sure if anything as good as Nominal Isabell exists for Coq. One can go quite far in defining 
> alpha-equivalence using the nominal techniques but the real problem is how to define a type of terms quotient with 
> alpha-equivalence.

Pitts in his overview of nominal techniques (Section 10 of [2]) points out that this is not quite trivial  to do nominal 
type theories constructively. I recall similar remarks by Christian Urban in his talks when he spoke about the issue of 
creating \alpha-quotient types out of existing ones. Some examples of what can go wrong are discussed by Andrew Swan 
[3,4], in particular decidability of freshness relation or the existence of a least finite support.

[2] https://www.cl.cam.ac.uk/~amp12/papers/nomt/nomt.pdf

[3] http://logicandanalysis.org/index.php/jla/article/download/274/109

[4] https://arxiv.org/abs/1702.01556

****

There is also the connection with HoTT and cubical stuff. Pitts mentions this in [2] above, but rather than focusing on 
how to use the nominal approach to model the Axiom of Univalence, I'd like to understand how to create and work with 
nominal datatypes in HoTT (a possibility mentioned in passing somewhere already by Voevodsky, if I recall correctly). If 
I am not mistaken, some recent work of Buchholtz seems to go in this direction:

http://www.math.lmu.de/~petrakis/buchholtz.pdf

https://github.com/UlrikBuchholtz/nominal-hott

Not sure if there are some developments in CoqHoTT along those lines and whether this is the right direction to go. 
Perhaps somebody more knowledgeable can step in and clarify this and other issues: what has been done, what could and/or 
should be done and what cannot/shouldn't be done.

Best,

t.