The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Hello,

On 2017-08-23 11:04, Talia Ringer 
<tringer AT cs.washington.edu>
 writes:

> I'm wondering if something like nominal Isabelle
> <https://nms.kcl.ac.uk/christian.urban/Nominal/> exists in Coq. I've found
> an extended abstract
> <http://www.seas.upenn.edu/~sweirich/papers/nominal-coq/lfmtp06.pdf> that
> discusses this, but I am yet to find follow-up work. I know there is a
> documented
> need for it <http://adam.chlipala.net/poplmark/>, so I'm wondering if
> anyone further work exists, and especially if there are any tools that
> people use, since I know that Nominal Isabelle is very popular.

You should watch the lectures of Stephanie Weirich from the DeepSpec
Summer School
(https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw/videos). The
relevant ones are the end of her second video (Part 20) and the third
video (Part 25).

The github repo for the lecture is here
https://github.com/DeepSpec/dsss17/tree/master/Stlc

Best,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2017-07: 407.07, 2016-07: 404.39

Attachment: signature.asc
Description: PGP signature