KEMBAR78
Daftar
Login
Programming with Refinement Types
Programming with Refinement Types
An Introduction to LiquidHaskell
Ranjit Jhala, Eric Seidel, Niki Vazou
[PDF]
1.
Introduction {#intro}
1.1.
Well-Typed Programs Do Go Wrong {#gowrong}
1.2.
Refinement Types
1.3.
Audience
1.4.
Getting Started
2.
Logic & SMT
2.1.
Syntax
2.2.
Semantics {#semantics}
2.3.
Verification Conditions
2.4.
Examples: Propositions
2.5.
Examples: Arithmetic
2.6.
Examples: Uninterpreted Function
2.7.
Recap
3.
Refinement Types
3.1.
Defining Types {#definetype}
3.2.
Errors
3.3.
Subtyping
3.4.
Writing Specifications
3.5.
Refining Function Types: Pre-conditions
3.6.
Refining Function Types: Post-conditions
3.7.
Testing Values: Booleans and Propositions {#propositions}
3.8.
Putting It All Together
3.9.
Recap
4.
Polymorphism {#polymorphism}
4.1.
Specification: Vector Bounds {#vectorbounds}
4.2.
Verification: Vector Lookup
4.3.
Inference: Our First Recursive Function
4.4.
Higher-Order Functions: Bottling Recursion in a
loop
4.5.
Refinements and Polymorphism {#sparsetype}
4.6.
Recap
5.
Refined Datatypes {#refineddatatypes}
5.1.
Sparse Vectors Revisited {#autosmart}
5.2.
Ordered Lists {#orderedlists}
5.3.
Ordered Trees {#binarysearchtree}
5.4.
Recap
6.
Boolean Measures {#boolmeasures}
6.1.
Partial Functions
6.2.
Lifting Functions to Measures {#usingmeasures}
6.3.
A Safe List API
6.4.
Recap
7.
Numeric Measures {#numericmeasure}
7.1.
Wholemeal Programming
7.2.
Specifying List Dimensions
7.3.
Lists: Size Preserving API
7.4.
Lists: Size Reducing API {#listreducing}
7.5.
Dimension Safe Vector API
7.6.
Dimension Safe Matrix API
7.7.
Recap
8.
Elemental Measures {#setmeasure}
8.1.
Talking about Sets
8.2.
Proving QuickCheck Style Properties {#quickcheck}
8.3.
Content-Aware List API {#listelems}
8.4.
Permutations
8.5.
Uniqueness
8.6.
Unique Zippers
8.7.
Recap
9.
Case Study: Okasaki's Lazy Queues {#lazyqueue}
9.1.
Queues
9.2.
Sized Lists
9.3.
Queue Type
9.4.
Queue Operations
9.5.
Recap
10.
Case Study: Associative Maps
10.1.
Specifying Maps {#mapapi}
10.2.
Using Maps: Well Scoped Expressions
10.3.
Implementing Maps: Binary Search Trees {#lemmas}
10.4.
Recap
11.
Case Study: Pointers & Bytes {#case-study-pointers}
11.1.
HeartBleeds in Haskell
11.2.
Low-level Pointer API
11.3.
A Refined Pointer API
11.4.
Assumptions vs Guarantees
11.5.
ByteString API
11.6.
Application API
11.7.
Nested ByteStrings
11.8.
Recap: Types Against Overflows
12.
Case Study: AVL Trees {#case-study-avltree}
12.1.
AVL Trees
12.2.
Specifying AVL Trees
12.3.
Smart Constructors
12.4.
Inserting Elements
12.5.
Rebalancing Trees
12.6.
Refactoring Rebalance
12.7.
Deleting Elements
12.8.
Functional Correctness