論文

査読有り
2011年

Program Calculation in Coq

ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY
  • Julien Tesson
  • ,
  • Hideki Hashimoto
  • ,
  • Zhenjiang Hu
  • ,
  • Frederic Loulergue
  • ,
  • Masato Takeichi

6486
開始ページ
163
終了ページ
+
記述言語
英語
掲載種別
研究論文(国際会議プロシーディングス)
DOI
10.1007/978-3-642-17796-5_10
出版者・発行元
SPRINGER-VERLAG BERLIN

Program calculation, being a programming technique that derives programs from specification by means of formula manipulation, is a challenging activity. It requires human insights and creativity, and needs systems to help human to focus on clever parts of the derivation by automating tedious ones and verifying correctness of transformations. Different from many existing systems, we show in this paper that Coq, a popular theorem prover, provides a cheap way to implement a powerful system to support program calculation, which has not been recognized so far. We design and implement a set of tactics for the Coq proof assistant to help the user to derive programs by program calculation and to write proofs in calculational form. The use of these tactics is demonstrated through program calculations in Coq based on the theory of lists.

Web of Science ® 被引用回数 : 6

リンク情報
DOI
https://doi.org/10.1007/978-3-642-17796-5_10
DBLP
https://dblp.uni-trier.de/rec/conf/amast/TessonHHLT10
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000290190700010&DestApp=WOS_CPL
URL
http://dblp.uni-trier.de/db/conf/amast/amast2010.html#conf/amast/TessonHHLT10
ID情報
  • DOI : 10.1007/978-3-642-17796-5_10
  • ISSN : 0302-9743
  • DBLP ID : conf/amast/TessonHHLT10
  • Web of Science ID : WOS:000290190700010

エクスポート
BibTeX RIS