Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Conducting a literature search

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Conducting a literature search


Chronological Thread 
  • 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

Archive powered by MHonArc 2.6.18.

Top of Page