Skip to content

ucsd-progsys/liquidhaskell-tutorial

Folders and files

NameName
Last commit message
Last commit date

Latest commit

077437f · Sep 30, 2024
Jul 30, 2023
Jul 30, 2023
Jul 30, 2023
Jul 30, 2023
Feb 11, 2015
Jul 30, 2023
Feb 2, 2018
Jul 31, 2023
Sep 30, 2024
Nov 22, 2017
Jul 19, 2023
Apr 3, 2016
Jul 24, 2020
Jul 30, 2023
Jul 30, 2023
Jul 30, 2023
Jul 23, 2020
Sep 30, 2024
Aug 10, 2015
Sep 30, 2024
Jul 24, 2020
Jul 30, 2023
Jul 30, 2023
Jul 18, 2023
Jun 29, 2023
Jul 26, 2020

Repository files navigation

LiquidHaskell Tutorial

TODO: UPDATE the website with the new code

NOTE The PDF/HTML are sometimes not up-to-date with the latest LiquidHaskell release. Please clone the github repository and run locally for best results.

How to Do The Tutorial

LH is available as a GHC plugin from version 0.8.10.

Thus, the best way to do this tutorial is to

Step 1 Clone this repository,

$ git clone https://github.com/ucsd-progsys/liquidhaskell-tutorial.git

Step 2: Iteratively edit-compile until it builds without any liquid type errors

$ cabal v2-build

or

$ stack build --fast --file-watch

The above workflow will let you use whatever Haskell tooling you use for your favorite editor, to automatically display LH errors as well.

Contents

Part I: Refinement Types

  1. Introduction
  2. Logic & SMT
  3. Refinement Types
  4. Polymorphism
  5. Refined Datatypes

Part II: Measures

  1. Boolean Measures
  2. Numeric Measures
  3. Set Measures

Part III : Case Studies

  1. Case Study: Okasaki's Lazy Queues
  2. Case Study: Associative Maps
  3. Case Study: Pointers & Bytes
  4. Case Study: AVL Trees

Update

$ git pull origin master
$ git submodule update --recursive

Building

Deploy on Github

$ cp package.yaml.pandoc package.yaml
$ mkdir _site dist
$ stack install pandoc
$ make html
$ make pdf
$ cp dist/pbook.pdf _site/book.pdf
$ git add _site
$ git commit -a -m "updating GH-PAGES"
$ git push --force-with-lease origin HEAD:gh-pages

Prerequisites

  • Install LaTeX dependencies:
    • Texlive
    • texlive-latex-extra
    • texlive-fonts-extra

Producing .pdf Book

$ make pdf
$ evince dist/pbook.pdf

Solutions to Exercises

Solutions are in separate private repo

TODO

A work list of TODO items can be found in the bug tracker

Feedback and Gotchas

Editing feedback and various gotchas can be found in feedback.md