Skip to content

ucsd-progsys/intro-refinement-types

Repository files navigation

README

This repository has the materials for a 120 minute tutorial on programming and proving with Refinement types with LiquidHaskell

For other versions, you may be interested in:

Running LiquidHaskell

  1. Try Online
  2. [VM Image][]
  3. Build Locally

Virtual Machine

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

Step 1 Download this VM image

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 Grab the source files from Github.

Build Slides

First

 $ git clone https://github.com/ucsd-progsys/liquid-client.git

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
  2. MathJax URL: change the relevant link in assets/templates/pagemeta.template
  3. Talk: change the TALK field in the Makefile which builds the src-$(TALK) directory.

Outline [120]

Part I: Basics

  • 01-index
  • 02-refinements
  • 03-datatypes
  • 04-case-study-insertsort

Part II: Proofs

  • 05-termination
  • 06-refinement-reflection
  • 07-map-reduce

Outline [25]

  • 01-intro [3]
  • 02-refinements [6]
  • 03-examples [9]
  • 04-abstracting [4]
  • 05-concl [3]

Editing Notes

To edit locally,

  1. Clone repositories
$ git clone https://github.com/ucsd-progsys/intro-refinement-types.git
$ cd intro-refinement-types
$ git clone https://github.com/ucsd-progsys/liquid-client.git
$ stack install
  1. Edit src-120/0X-file.lhs

  2. stack exec -- make

  3. open dist/_site/*X-file.html

To upload do,

  1. make upload

Misc Links

Extra

  • 05-case-study-eval
  • 06-case-study-bytestring
  • 07-abstract-refinements
  • 08-bounded-refinements
  • 15-security
  • Tagged.lhs

WBL Heaps

Insert Sort