12_Conclusion.lhs

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

Conclusion
----------

<div class="hidden">

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

</div>

Conclusion
==========

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


Use **Types** to lift **Logic + Analysis** to Modern Programs 

<br>

<div class="fragment"> 

-------------------       ------------------------------------------------
**Properties:**           Predicates *+ Types*
**Proofs:**               Verification Conditions *+ Subtyping* 
**Inference:**            Abstract Interpretation *+ Hindley-Milner*
-------------------       ------------------------------------------------

</div>


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

Use **Types** to lift **Logic + Analysis** to Modern Programs 

<br>

**Take Home: Types are a simple and uniform way to analyze**

+ Unbounded Data (eg. Arrays, Lists, HashMaps)
+ Polymorphism   (eg. Generics,...)
+ Callbacks/HOFs (eg. map, reduce, filter,...)

<div class="hidden">

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

Use **Types** to lift **Logic + Analysis** to Modern Programs 

<br>

**Take Home 2: Uninterpreted Functions**

+ Measures for Datatype properties

+ Abstract Refinements 

</div>

Current & Future Work
---------------------

**Technology**

+ Speed
+ Imperative Features (Pointers, Mutation, ...) 
+ Diagnostics & *Error Messages*

Current & Future Work
---------------------

**Applications**

+ Concurrency & Distribution
+ Probabilistic Behavior
+ Completion, Repair & Synthesis

 {#asd}
=======

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

<br>

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

<br>