If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis: http://goto.

If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis: http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf The UCSD Programming Systems lab has also applied refinement types to dynamic languages[1] and systems programming languages[2]. The MIT Computer Assisted Programming Group has similarly used liquid types-based techniques for program synthesis[3], while a group at Purdue has been working on maching learning of complex refinement types[4,5] that are difficult to state or infer using the liquid types techniques. [1] http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf [2] http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.pdf http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.p... [3] http://people.csail.mit.edu/polikarn/publications/pldi16.pdf http://people.csail.mit.edu/polikarn/publications/pldi16.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/icfp_my_version.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [5] https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf