TY - GEN

T1 - Verifying relational properties of functional programs by first-order refinement

AU - Asada, Kazuyuki

AU - Sato, Ryosuke

AU - Kobayashi, Naoki

N1 - Publisher Copyright:
© 2015 ACM.

PY - 2015/1/13

Y1 - 2015/1/13

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84947297507&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947297507&partnerID=8YFLogxK

U2 - 10.1145/2678015.2682546

DO - 10.1145/2678015.2682546

M3 - Conference contribution

AN - SCOPUS:84947297507

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

SP - 61

EP - 72

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

PB - Association for Computing Machinery, Inc

T2 - ACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015

Y2 - 13 January 2015 through 14 January 2015

ER -