# Papers etc.

## Papers

To learn about the theory behind Liquid Types, I recommend reading first the
PLDI 2008 paper and then the ESOP 2013 paper. Alternatively, one lazy weekend,
you could curl up with:

+ [Pat Rondon's Ph.D Dissertation](http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf)
+ [Tech Report](http://goto.ucsd.edu/~rjhala/liquid/liquid_types_techrep.pdf)

### Haskell

- [Refinement Types For Haskell, ICFP 2014](http://goto.ucsd.edu/~rjhala/papers/refinement_types_for_haskell.pdf)
- [LiquidHaskell in the Real World, Haskell 2014](http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf)
- [Abstract Refinement Types, ESOP 2013](http://goto.ucsd.edu/~rjhala/papers/abstract_refinement_types.pdf)


### ML

- [Liquid Types, PLDI 2008](http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf)
- [Type-based Data Structure Verification, PLDI 2009](http://goto.ucsd.edu/~rjhala/papers/type-based_data_structure_verification.pdf)
- [Dsolve: Safety Verification via Liquid Types, CAV 2010](http://goto.ucsd.edu/~rjhala/papers/safety_verification_with_liquid_types.pdf)
- [HMC: Verifying Functional Programs with Abstract Interpreters, CAV 2011](http://goto.ucsd.edu/~rjhala/papers/hmc.pdf)

### C

- [Low-level Liquid Types, POPL 2010](http://goto.ucsd.edu/~rjhala/liquid/low_level_liquid_types.pdf)
- [Deterministic Parallelism With Liquid Effects, PLDI 2012](http://goto.ucsd.edu/~rjhala/papers/deterministic_parallelism_via_liquid_effects.pdf)
- [Verifying C With Liquid Types, CAV 2012](http://goto.ucsd.edu/~rjhala/papers/csolve_verifying_c_with_liquid_types.pdf)


## Talks

The following talks are good tutorial introductions to the techniques.

- [Tutorial at VMCAI](http://goto.ucsd.edu/~rjhala/talks/liquid_types_VMCAI.pptx)
- [Tutorial at CAV](http://goto.ucsd.edu/~rjhala/talks/liquid_types_CAV2011.pptx)

## People

Liquid Types have been developed in the UCSD Programming Systems group by

- [Alexander Bakst](http://cseweb.ucsd.edu/~abakst)
- [Ranjit Jhala](http://cseweb.ucsd.edu/~rjhala)
- [Ming Kawaguchi](http://cseweb.ucsd.edu/~mwookawa)
- [Patrick Rondon](http://cseweb.ucsd.edu/~prondon)
- [Eric Seidel](http://cseweb.ucsd.edu/~eseidel)
- [Michael Smith](https://spinda.net)
- [Anish Tondwalkar](https://github.com/atondwal)
- [Chris Tetreault](https://github.com/christetreault)
- [Niki Vazou](http://cseweb.ucsd.edu/~nvazou)

## Thanks

This work is funded by NSF grants CCF-0644361, CNS-0720802, CCF-0702603, and generous gifts from Microsoft Research.