Verification with Refinement Types

Introduction

Part I: Refinements 101

Case Study: Vector Bounds

Part II: Properties of Structures

Case Study: Sorting, Interpreter

Part III: Invariants of Data Structures

Case Study: Sorting actually Sorts Lists

Part IV: Termination and Correctness Proofs

Case Study: Optimizing Expressions, Search Trees