Giter VIP home page Giter VIP logo

liquidhaskell-tutorial's Introduction

LiquidHaskell Tutorial

TODO: UPDATE the website with the new code

$ stack install pandoc pandoc-citeproc template

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.

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. Elemental 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

Get Started

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

$ stack install
$ export PATH=~/.local/bin:$PATH

$ stack exec -- liquid ./src/01-intro.lhs
$ stack exec -- liquid ./src/02-logic.lhs
$ stack exec -- liquid ./src/03-basic.lhs
$ stack exec -- liquid ./src/04-poly.lhs
$ stack exec -- liquid ./src/05-datatypes.lhs
$ stack exec -- liquid ./src/06-measure-bool.lhs
$ stack exec -- liquid ./src/07-measure-int.lhs
$ stack exec -- liquid ./src/08-measure-sets.lhs
$ stack exec -- liquid ./src/09-case-study-lazy-queues.lhs
$ stack exec -- liquid ./src/10-case-study-associative-maps.lhs
$ stack exec -- liquid ./src/11-case-study-pointers.lhs
$ stack exec -- liquid ./src/12-case-study-AVL.lhs

Update

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

Building

Deploy on Github

Dependencies

$ stack install pandoc
Prerequisites
$ cd ../ && git clone https://github.com/ucsd-progsys/liquid-client.git
Actual deployment
$ git checkout master
$ make html
$ cp -r _site ~/tmp/
$ git checkout gh-pages
$ cp -r ~/tmp/* .
$ git commit -a
$ git push origin gh-pages

Compiling .pdf

Dependencies

$ stack install pandoc pandoc-citeproc template

Prerequisites

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

To install LaTeX dependencies on Ubuntu 17.10, following them:

$ sudo apt install -y texlive-latex-base 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

liquidhaskell-tutorial's People

Contributors

ranjitjhala avatar waddlaw avatar gridaphobe avatar nikivazou avatar alanz avatar christetreault avatar rakeshgk avatar bandali0 avatar pseudonom avatar skyzh avatar adinapoli avatar crabmusket avatar mmport80 avatar robkorn avatar y-taka-23 avatar tjade273 avatar

Stargazers

Daniel Kahlenberg avatar

Watchers

 avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.