coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Nominal reasoning in Coq

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Nominal reasoning in Coq
Date: Wed, 23 Aug 2017 11:04:42 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-vk0-f65.google.com
Ironport-phdr: 9a23:KkwcwhwoanW4I4bXCy+O+j09IxM/srCxBDY+r6Qd0uwXIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi56idXERHiPyJ0IP70E8jclZeZzee3rqHaZwRBzAC8Z7x/Nl3isR/QsMYbm6NpMeAuwwDJo31HZ+NQg25kOATAzF7H+s6s8cs7oGxrsPU7+psYXA==

Hi all,

I'm wondering if something like nominal Isabelle exists in Coq. I've found an extended abstract that discusses this, but I am yet to find follow-up work. I know there is a documented need for it, 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.

If there is no analogue, I'm curious if anyone knows whether this is fundamental to the difference in logics between Coq and Isabelle, or whether this is "just" a matter of someone building an analogous effective tool in Coq itself.

Thanks!

Talia

[Coq-Club] Nominal reasoning in Coq, Talia Ringer, 08/23/2017
- Re: [Coq-Club] Nominal reasoning in Coq, Abhishek Anand, 08/24/2017
- Re: [Coq-Club] Nominal reasoning in Coq, Alan Schmitt, 08/24/2017