12_Conclusion.lhs

 {#ASda}
========

Conclusion
----------

<div class="hidden">

\begin{code}
main = putStrLn "Easter Egg: to force Makefile"
\end{code}

</div>

Conclusion
==========


Liquid Types 
------------

Generalize Program **Logics** via **Types**

<br>

<div class="fragment">Expressive *and* Automatic</div>


Liquid Types 
------------

Generalize Program **Logics** via **Types**

<br>

Expressive *and* Automatic

<br>

**Take Home 1: Inference**

+ Typecheck "templates" 

+ Abstract Interpretation
 
Liquid Types 
------------

Generalize Program **Logics** via **Types**

<br>

Expressive *and* Automatic

<br>

**Take Home 2: Uninterpreted Functions**

+ Measures for Datatype properties

+ Abstract Refinements 
 
Liquid Types 
------------

Generalize Program **Logics** via **Types**

<br>

Expressive *and* Automatic

<br>

**Take Home 3: Laziness breaks *partial* correctness**
 
+ Use refinements prove termination

+ Use termination to prove refinements

<!--

Take Home Messages
------------------

1. <div class="fragment"> **Inference**
    + Typecheck "templates" 
    + Abstract Interpretation
   </div>


2. <div class="fragment">**Uninterpreted functions**
    + Measures for Datatype properties
    + Abstract Refinements 
   </div>

3. <div class="fragment">**Laziness breaks *partial* correctness**
    + Use refinements prove termination
    + Use termination to prove refinements
   </div>


Future Work
-----------

<br>
<br>

- <div class="fragment">Speed</div>

- <div class="fragment">Case Studies</div>

- <div class="fragment">**Error Feedback**</div>

-->

 {#asd}
=======

Thank You!
----------

<br>

[`http://goto.ucsd.edu/liquid`](http://goto.ucsd.edu/liquid)

<br>