conclusion.tex

\chapter{Conclusion}
In this thesis we presented various refinement type systems.
We started with type systems where the refinement language expresses arbitrary program expressions.
Even though these systems are expressive, the assertions formed can not be statically
verified. 
%
To reason in such systems, we presented two alternatives:
interactive theorem proving, where 
the user should provide explicit proofs, and 
contracts calculi, where 
the assertions are verified at runtime.
%
Next we presented refinement type system 
which restrict the refinement language, 
so as to render type checking decidable.
%thus both type checking and inference
%is decidable.
As an example, we presented Liquid Types, in which 
the refinement language is restricted according to a finite set of qualifiers
and allows not only decidable verification, but also automatic type inference.
Then, we presented Abstract Refinement Types, which can be used
in a refinement type system to enhance expressiveness without increasing complexity.
Then,  we present \toolname
that combines liquidTypes with abstraction over refinements
to enhance expressiveness of LiquidTypes.
\toolname is a quite expressive verification tool for Haskell programs 
that can be used to check termination, 
totality  and general functional correctness.
Finally, we evaluate \toolname in real world Haskell libraries.