**Ranjit Jhala** University of California, San Diego

Joint work with: N. Vazou, E. Seidel, P. Rondon, M. Kawaguchi D. Vytiniotis, S. Peyton-Jones

**Refinement Types**

**Data Structures**

**Low-level Memory Safety**

**Evaluation**

**Conclusion**