Although a plethora of programming languages provide developers with robust type systems that describe legal sets of values for various operations, eliminating the possibility of runtime errors beforehand. However, well-typed programs do go wrong due to errors like division by zero, buffer overflow, and many other logic bugs that cannot be checked by types. It is intuitive for us to further constrain the set of values inhabited by a type using some sort of first-order logic predicates like int[x | 0 < x and x < 100] where this integer has type $(x: \mathbb{N} \to x \in (0, 100))$.Thus a variable $x = -1$ becomes ill-typed for int[x | 0 < x and x < 100].
Refinements are essentially predicates drawn from decidable logics. Type checking on refinement types yields constraints whose validity implies that the program is well-typed and free of logic bugs. All the constraints (more precisely, the verification condition) can be efficiently translated into a SMT expression and be checked for satisfiability. A VC is either a quantifier free predicate $p$, or a conjunction of two sub-constraints $c_1 \wedge c_2$, or an implication of the form $\forall x:\tau.p \to c$ which says that for all $x$ inhabited by a type $\tau$, if $p$ holds, then it must be the case that $c$ holds.
Readers familiar with simply type lambda calculus will find this section easy to follow. We will demonstrate how RT is integrated to STLC. Consider the following extended syntax for STLC:
Example: Consider the entailment judgment $\Gamma;x:int\{ 0 \le x \}; y:int\{ y = x + 1 \} \vdash 0 \le y$. It reduces by inverse lemma using the Ent-Ext rule to the following verification condition:
$$ \Gamma \vdash \forall x:int.(0 \leq x) \Rightarrow \forall y.int.(y = (x + 1)) \Rightarrow (0 \le y) $$