README.md

README

This repository has the materials for a 2-hour workshop on Programming with Refinement Types which is also a tutorial introduction to LiquidHaskell.

Running LiquidHaskell

You can run this code in any of the following ways:

1. Online

2. Virtual Machine

3. Build LiquidHaskell

The online web demo is easiest for the workshop. See below

Option 1: Online

This is the easiest by far; point your browser here

Option 2: Virtual Machine

This is also very easy, if you can manage the 2Gb download.

Step 1 Download this VM image

he code files are in lh-workshop/src/*.lhs

Step 2 Choose your editor. For emacs do:

   tar -zxvf liquid-emacs.tgz

and for Spacemacs (a great Vim-Emacs hybrid) do:

   tar -zxvf liquid-spacemacs.tgz

Step 3 The code files are in

   ~/lh-workshop/src/*.lhs

Option 3: Local Build

Finally, if you prefer, you can build LiquidHaskell from:

1. cabal

2. github

Build Slides

To build rust-style html (in dist/_site)

 $ stack exec -- make html

To build reveal.js slides (in dist/_slides)

 $ stack exec -- make slides

Edit Slides

You can modify the following parameters:

1. Server URL: change liquidserver in assets/templates/preamble.lhs

Misc Links

WBL Heaps

• HS+DT proof
• HS
• HS+Liquid

Insert Sort

• https://github.com/davidfstr/idris-insertion-sort/tree/master
• http://www.enseignement.polytechnique.fr/informatique/INF551/TD/TD5/aux/Insert_Sort.v
• https://github.com/goldfirere/singletons/blob/master/tests/compile-and-dump/InsertionSort/InsertionSortImp.hs