content: 
  
   {#ASD}
  =======
  
  Liquid Types For Haskell
  ------------------------
  
  
  <br>
  <br>
  
  **Ranjit Jhala**
  
  University of California, San Diego
  
  <br>
  <br>
  
  
  Joint work with: 
  
  N. Vazou, E. Seidel, P. Rondon, D. Vytiniotis, S. Peyton-Jones
  
  
  <div class="hidden">
  
  \begin{code}
  main = putStrLn "Easter Egg: to force Makefile"
  \end{code}
  
  </div>
  
  
  Well-Typed Programs Can Go Wrong
  ================================
  
   {#asd}
  -------
  
  Division By Zero
  ----------------
  
  <div class="fragment"> 
  \begin{code} <div/> 
  λ> let average xs = sum xs `div` length xs
  
  λ> average [1,2,3]
  2
  \end{code}
  </div>
  
  <div class="fragment"> 
  
  \begin{code} <br> 
  λ> average []
  *** Exception: divide by zero
  \end{code}
  
  </div>
  
  Missing Keys
  ------------
  
  <div class="fragment"> 
  \begin{code} <div/> 
  λ> :m +Data.Map 
  λ> let m = fromList [ ("haskell", "lazy")
                      , ("ocaml"  , "eager")]
  
  λ> m ! "haskell"
  "lazy"
  \end{code}
  </div>
  
  <div class="fragment"> 
  \begin{code} <br> 
  λ> m ! "javascript"
  "*** Exception: key is not in the map
  \end{code}
  </div>
  
  Segmentation Faults
  -------------------
  
  <div class="fragment"> 
  \begin{code} <div/> 
  λ> :m +Data.Vector 
  λ> let v = fromList ["haskell", "ocaml"]
  λ> unsafeIndex v 0
  "haskell"
  \end{code}
  </div>
  
  <div class="fragment"> 
  \begin{code} <br> 
  λ> V.unsafeIndex v 3
  
  
  'ghci' terminated by signal SIGSEGV ...
  \end{code}
  </div>
  
  
  "HeartBleeds"
  -------------
  
  \begin{code} <div/>
  λ> :m + Data.Text Data.Text.Unsafe 
  λ> let t = pack "Kanazawa"
  λ> takeWord16 5 t
  "Kanaz"
  \end{code}
  
  <br>
  
  <div class="fragment"> 
  Memory overflows **leaking secrets**...
  
  <br>
  
  \begin{code} <div/>
  λ> takeWord16 20 t
  "kamakura\1912\3148\SOH\NUL\15928\2486\SOH\NUL"
  \end{code}
  </div>
  
  Goal
  ----
  
  Extend Hindley-Milner To Prevent More Errors
  
  Liquid Types for Haskell
  ========================
  
  LiquidHaskell
  -------------
  
  <br>
  <br>
  
  <div class="fragment">Refine **types** with **predicates**</div>
  
  <br>
  <br>
  
  <div class="fragment">**Expressive** specification & **Automatic** verification</div>
  
  
  
  Automatic
  ---------
  
  [Liquid Types, PLDI 08](http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf)
  
  <br>
  
  + Abstract Interpretation 
  
  + SMT Solvers 
  
  Expressive
  ----------
  
  <br>
  <br>
  
  This talk ...
  
  Try Yourself
  ------------
  
  <br>
  
  **google: ** `"liquidhaskell demo"` 
  
   {#zog} 
  --------
  
  <br>
  <br>
  <br>
  <br>
  
  [[continue]](01_SimpleRefinements.lhs.slides.html)
  
  
  Plan 
  ----
  
  1. <a href="01_SimpleRefinements.lhs.slides.html" target= "_blank">Refinements
  2. <div class="fragment"><a href="02_Measures.lhs.slides.html" target= "_blank">Measures</a></div>
  3. <div class="fragment"><a href="03_HigherOrderFunctions.lhs.slides.html" target= "_blank">Higher-Order Functions</a></div>
  4. <div class="fragment"><a href="04_AbstractRefinements.lhs.slides.html" target= "_blank">Abstract Refinements:</a> <a href="06_Inductive.lhs.slides.html" target="_blank">Code</a>, <a href="08_Recursive.lhs.slides.html" target= "_blank">Data</a>,<a href="07_Array.lhs.slides.html" target= "_blank">...</a>,<a href="05_Composition.lhs.slides.html" target= "_blank">...</a></div>
  5. <div class="fragment"><a href="09_Laziness.lhs.slides.html" target="_blank">Lazy Evaluation</a></div>
  6. <div class="fragment"><a href="10_Termination.lhs.slides.html" target="_blank">Termination</a></div>
  7. <div class="fragment"><a href="11_Evaluation.lhs.slides.html" target="_blank">Evaluation</a></div>
  
  