arXiv:1711.09281cs.PL
Refinement Types for Ruby
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
Abstract
Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is built on top of RDL, a Ruby type checker that provides basic type information for the verification process. RTR works by encoding its verification problems into Rosette, a solver-aided host language. RTR handles mixins through assume-guarantee reasoning and uses just-in-time verification for metaprogramming. We formalize RTR by showing a translation from a core, Ruby-like language with refinement types into Rosette. We apply RTR to check a range of functional correctness properties on six Ruby programs. We find that RTR can successfully verify key methods in these programs, taking only a few minutes to perform verification.
There are a bunch of interesting stuff coming along. I don't know if you have seen the Refinement types in Ruby paper based on RDL recently published in VMCAI [1], this opens the window to verification of Ruby code. [1]: https://arxiv.org/abs/1711.09281
sankha93View on HNParent context