Refinement types are a type-based, static verification technique designed to be practical. They enrich the types of an existing programming language with logical predicates to specify program properties and automatically validate these specifications using SMT solvers. Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real world applications, e.g., safety of cryptographic protocols, memory and resource usage, and web security. But, the weakness of refinement types is that they do not meet the soundness standards set by theorem provers.

In this talk, we will see a brief overview of refinement types, the consequences of their practical design, and the presenter’s future goals on the establishment of soundness.