coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Conducting a literature search

From: Kenneth Roe <kendroe AT hotmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Conducting a literature search
Date: Fri, 8 Sep 2017 22:57:49 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=SoftFail smtp.mailfrom=kendroe AT hotmail.com; spf=None smtp.helo=postmaster AT nm26.bullet.mail.ne1.yahoo.com
Ironport-phdr: 9a23:fEStcBwe4AqqzpnXCy+O+j09IxM/srCxBDY+r6Qd0u8SIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi56idXERHiPyJ0IP70E8jclZeZzee3rr7eZQNFmDr1W7R/ZEG1oAPdrM4bqYtlNqM4yx+PqXxNLbcFjVh0LE6eyk6vrvy7+4Rupnxd

I am getting ready to release a term rewriting/expression simplification Coq
plugin within about the next month. I actually developed this code in the
early 90s but recently realized the system would be useful for the Coq
theorem prover. The plugin will give Coq a simplification system similar to
what exists in Isabelle.

Right now, I want to collect up literature in the field (so I can publish a
research paper). Can people on the mailing list point me to related work
references that are of interest?

- Ken

[Coq-Club] Conducting a literature search, Kenneth Roe, 09/09/2017