Email Gateway (Apr 23 2022 at 15:31): Email Gateway (Apr 23 2022 at 15:31):From: Joachim Breitner <mail@joachim-breitner.de>
Hello,
it’s been many years since I touched Isabelle and the Nominal2 package,
but I keep bragging about this way of handling bindings when talking to
users of Coq etc.
I might want to do some PLTish experiments, and maybe I’ll just try to
use Isabelle and Nominal2 again. But I can’t find a manual or tutorial
to refresh my memory… it seems that
https://isabelle.in.tum.de/nominal/download.html
is rather out of date, and
https://www.isa-afp.org/entries/Nominal2.html
contains the code, but not much in terms of guidance.
I also found https://lmcs.episciences.org/813 which seems useful. Maybe
it should be linked from the two places above?
Is there any other material worth knowing?
(I just noticed that my own thesis has a intro section on nominal logic
and Nominal, but only very cursory, of course:
https://www.joachim-breitner.de/thesis/diss.pdf )
Cheers,
Joachim
Email Gateway (Apr 24 2022 at 22:41):From: "\"Urban, Christian\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear Joachim,
Yes, unfortunately documentation is lacking. The link
is indeed outdated, but Nominal2 made it into the AFP as a module and the code is maintained for the latest Isabelle (as I am writing Isabelle 2021-1). In addition to the paper you quote, the following paper might be useful in order to understand how atoms and permutations work in Nominal 2 (vs Nominal 1).
Hope this helps,
Christian
Email Gateway (Apr 24 2022 at 22:42):From: "\"Urban, Christian\"" <cl-isabelle-users@lists.cam.ac.uk>
Sorry link is here:
https://nms.kcl.ac.uk/christian.urban/Publications/nominal-atoms.pdf
Christian
Last updated: Apr 23 2024 at 20:15 UTC