@inproceedings{zhu2015learning,
author = {Zhu, He and Nori, Aditya and Jagannathan, Suresh},
title = {Learning Refinement Types},
booktitle = {International Conference on Functional Programming (ICFP)},
year = {2015},
month = {August},
abstract = {We propose the integration of a random test generation system(capable of discovering program bugs) and a refinement type system (capable of expressing and verifying program invariants), for higher-order functional programs, using a novel lightweight learning algorithm as an effective intermediary between the two. Our approach is based on the well-understood intuition that useful, but difficult to infer, program properties can often be observed from concrete program states generated by tests; these properties act as likely invariants, which if used to refine simple types, can have their validity checked by a refinement type checker. We describe an implementation of our technique for a variety of benchmarks written in ML, and demonstrate its effectiveness in inferring and proving useful invariants for programs that express complex higher-order control and dataflow.},
publisher = {ACM - Association for Computing Machinery},
url = {http://approjects.co.za/?big=en-us/research/publication/learning-refinement-types/},
edition = {International Conference on Functional Programming (ICFP)},
}