coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Are there any tools that implement the refinement rules in the book "programming from specification"?

From: 周晓宇 <zhouxy AT seu.edu.cn>
To: coq-club AT inria.fr
Subject: [Coq-Club] Are there any tools that implement the refinement rules in the book "programming from specification"?
Date: Thu, 16 Mar 2017 09:06:26 +0800 (GMT+08:00)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=zhouxy AT seu.edu.cn; spf=Pass smtp.mailfrom=zhouxy AT seu.edu.cn; spf=Pass smtp.helo=postmaster AT seu.edu.cn
Ironport-phdr: 9a23:BqALMB/OTa0t5P9uRHKM819IXTAuvvDOBiVQ1KB51egcTK2v8tzYMVDF4r011RmSDNidtqMP0LeempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwVFiCC9bL52Ixm7owXcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh8WHZhMx+grxGrhy7oBJw34HbboKOOfVkYq/QZ8gVSHBdUstTUSFKH4Oyb5EID+oEJetaqY//pV0Tpha5BAisBOTvyiJHh372xqA6yPouERzc0AM+At0OrW7Yo8nzNKoLV+2+0arGzS3bYv9Lxzvx9ZLEfg4urPyPR759cNbdxVMvGg/bllmct5LpMj2P2ukDqWSW7OttWfixh2I5pAx8pCWkyN02hYnTnI0Vz0jJ9SVnz4YxIt21UFV7bsC5EJdKqS6VKpZ2Ttk+TGFuoCo6y7sGtoCnfCUS1Zgr2QPTZ+aZf4WH4R/vTuecLStiiH9lZr6znxOy/lKhyu34WMm0ylFKri9dn9jNtnAN0AHT68eHS/Zm5UeuxyuP2xrN5e5ZPEA4j7bUK5g5zr4qipUTqVjDHjPxmEjukKCWcVwk9vG05OTjf7XpvYSRN5R0iwH7KqQhgNazAeU+MggUXmiU4/6w1LP5/R6xfLIfhfov16LdrZryJMIBp6f/DRUG/Jwk7kNH98/uhMYYmmQXPXpedQ/BgoT0fVrIdqOrRcyjikihxW84j8vNOafsV83A

Hi Coq-Club:

I am reading the book "programming from specification". There are a variety of refinement rules in the book. Are there any theorem provers that prove the rules and implement them as some kind of refinement tactics? If there isn't any implementation of there rules, why?

thanks.

Xiaoyu Zhou

Southeast University

[Coq-Club] Are there any tools that implement the refinement rules in the book "programming from specification"?, 周晓宇, 03/16/2017