論文

査読有り
2003年

Correctness of a higher-order removal transformation through a relational reasoning

PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS
  • S Nishimura

2895
開始ページ
358
終了ページ
375
記述言語
英語
掲載種別
研究論文(学術雑誌)
出版者・発行元
SPRINGER-VERLAG BERLIN

The syntactic logical relations developed by Pitts are applied to show the correctness of a higher-order removal program transformation algorithm. The convenient proof method that resorts to the induction on the structure of programs does not apply because of the circular references to be introduced by the transformation. Using a variant of the syntactic logical relations, in which every pair of the transformation source and target are related, one can break the circularity and make an inductive proof go through. This demonstrates that the syntactic logical relations provide a basis of another general proof method for showing the correctness of program transformations.

Web of Science ® 被引用回数 : 4

リンク情報
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000187786700024&DestApp=WOS_CPL
ID情報
  • ISSN : 0302-9743
  • Web of Science ID : WOS:000187786700024

エクスポート
BibTeX RIS