Verifying relational properties of functional programs by first-order refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

Much progress has been made recently on fully automated verification of higher-order functional programs, based on refinement types and higher-order model checking. Most of those verification techniques are, however, based on first-order refinement types, hence unable to verify certain properties of functions (such as the equality of two recursive functions and the monotonicity of a function, which we call relational properties). To relax this limitation, we introduce a restricted form of higher-order refinement types where refinement predicates can refer to functions, and formalize a systematic program transformation to reduce type checking/inference for higher-order refinement types to that for first-order refinement types, so that the latter can be automatically solved by using an existing software model checker. We also prove the soundness of the transformation, and report on implementation and experiments.

Original languageEnglish
Pages (from-to)2-62
Number of pages61
JournalScience of Computer Programming
Volume137
DOIs
Publication statusPublished - 2017 Apr 1

Keywords

  • Automated verification
  • Higher-order functional language
  • Refinement types

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Verifying relational properties of functional programs by first-order refinement'. Together they form a unique fingerprint.

  • Cite this