Verifying relational properties of functional programs by first-order refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 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 preliminary implementation and experiments.

Original languageEnglish
Title of host publicationPEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015
PublisherAssociation for Computing Machinery, Inc
Pages61-72
Number of pages12
ISBN (Electronic)9781450332972
DOIs
Publication statusPublished - Jan 13 2015
Externally publishedYes
EventACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015 - Mumbai, India
Duration: Jan 13 2015Jan 14 2015

Publication series

NamePEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015

Other

OtherACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015
CountryIndia
CityMumbai
Period1/13/151/14/15

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Computer Vision and Pattern Recognition
  • Software

Cite this

Asada, K., Sato, R., & Kobayashi, N. (2015). Verifying relational properties of functional programs by first-order refinement. In PEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015 (pp. 61-72). (PEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015). Association for Computing Machinery, Inc. https://doi.org/10.1145/2678015.2682546