**1.**Case Study: Sorting Lists (Revisited)**1.1.**Exercise: Insertion Sort actually Sorts**1.2.**Exercise: Merge Sort actually Sorts**1.3.**Invariants In Constructors**1.4.**Abstracting Refinements**1.5.**Abstracting Refinements**1.6.**Abstracting Refinements**1.7.**Abstracting Refinements**1.8.**Abstract Refinements: Insertion Sort**1.9.**Abstract Refinements: Merge Sort**1.10.**Recap: Invariant via Refined Constructors**1.11.**Plan**2.**Verification with Refinement Types**3.**Verification with Refinement Types**4.**Case Study: Interpreting an Imperative Language**4.1.**Proving Something is Impossible**4.2.**Proving Something is Impossible**4.3.**State**4.4.**Arithmetic Expressions**4.5.**Evaluating Arithmetic Expressions**4.6.**Variables Read in an Expression**4.7.**Statements**4.8.**Evaluating Statements**4.9.**Specify Used-Before-Defined Variables**4.10.**Statically Verifying a Dynamic Check**4.11.**Some Safe and Unsafe Programs**4.12.**Plan**5.**Basic Refinement Types**5.1.**Types**5.2.**Predicates**5.3.**Predicates**5.4.**Predicates**5.5.**Predicates**5.6.**Predicates**5.7.**Example: "Singletons"**5.8.**Example: Natural Numbers**5.9.**A Term Can Have*Many*Types**5.10.**1. Predicate Subtyping [NUPRL, PVS]**5.11.**1. Predicate Subtyping [NUPRL, PVS]**5.12.**1. Predicate Subtyping [NUPRL, PVS]**5.13.**Example: Natural Numbers**5.14.**Example: Natural Numbers**5.15.**2. Typing Applications (Function Calls)**5.16.**2. Typing Applications (Function Calls)**5.17.**2. Typing Applications (Function Calls)**5.18.**2. Typing Applications (Function Calls)**5.19.**2. Typing Applications (Function Calls)**5.20.**2. Typing Applications (Function Calls)**5.21.**2. Typing Applications (Function Calls)**5.22.**Recap: Basic Refinement Types**5.23.**Recap: Basic Refinement Types**5.24.**Recap: Refinement Types 101**5.25.**Plan**6.**Code is meant to be run...**6.1.**Code is meant to be run...**6.2.**Code is meant to be run...and finish!**6.3.**Avoiding Infinite Loops**6.4.**Lets prove termination!**6.5.**Example: Proving Termination of`sum`

**6.6.**Proving Termination**6.7.**Proving Termination**6.8.**Proving Termination**6.9.**Proving Termination**6.10.**Example: Proving Termination of`sum`

**6.11.**User Specified Termination Metrics**6.12.**User Specified Termination Metrics**6.13.**User Specified Termination Metrics**6.14.**Proving Termination**6.15.**Lexicographic Termination**6.16.**How About Data Types?**6.17.**User specified metrics on Data Types**6.18.**Termination Can be Tricky**6.19.**Avoiding Infinite Loops**6.20.**Avoiding Infinite Loops**6.21.**Avoiding Infinite Loops**6.22.**Avoiding Infinite Loops**6.23.**Avoiding Infinite Loops is Easy (in Practice)**6.24.**Avoiding Infinite Loops is Easy (in Practice)**6.25.**Avoiding Infinite Loops is Easy (in Practice)**6.26.**Avoiding Infinite Loops is Easy (in Practice)**6.27.**Plan**7.**Binary Search Trees**7.1.**Binary Search Trees**7.2.**Legal Binary Search Trees**7.3.**Lookup a Value in a BST**7.4.**Update a Value in a BST**7.5.**What Theorems Shall we Prove?**7.6.**Functional Correctness: McCarthy's Dictionary Laws**7.7.**Specifying the Laws as Types**7.8.**Verifying the Laws as Types**7.9.**Verifying the Laws as Types**7.10.**Verification with Refinement Types**7.11.**Language Integrated Verification**8.**Types as Propositions, Programs as Proofs**8.1.**Types As Propositions**8.2.**Types as Propositions: Example**8.3.**Programs As Proofs: Example**8.4.**Types as Propositions**8.5.**Types as Propositions: Example**8.6.**Programs As Proofs: Example**8.7.**Types as Propositions, Programs as Proofs**8.8.**Those Proofs were Boring**8.9.**Those Proofs were Boring**8.10.**Theorems about Functions**8.11.**Refinement Reflection**8.12.**Reflect Function into Output Type**8.13.**Reflect Function into Output Type**8.14.**Reflection at Result Type**8.15.**Structuring Proofs as Calculations**8.16.**Structuring Proofs as Calculations**8.17.**Types as Propositions, Programs as Proofs**8.18.**Reusing Proofs: Functions as Lemmas**8.19.**Reusing Proofs: Functions as Lemmas**8.20.**Reusing Proofs: Functions as Lemmas**8.21.**Types as Propositions, Programs as Proofs**8.22.**Types as Propositions, Programs as Proofs**8.23.**Proof by Logical Evaluation**8.24.**Proof by Logical Evaluation**8.25.**Proof by Logical Evaluation**8.26.**Proof by Induction**8.27.**Proof by Induction**8.28.**Proof by Induction**8.29.**Types as Propositions, Programs as Proofs**8.30.**Types as Propositions, Programs as Proofs**8.31.**Types as Propositions, Programs as Proofs**8.32.**Theorems about Data**8.33.**Theorems about Data: Associativity of`append`

**8.34.**Types as Propositions, Programs as Proofs**8.35.**Plan**9.**Invariants of Data Structures**9.1.**Invariants of Data Structures**9.2.**Recall: Properties of Structures**9.3.**Recall: Properties of Structures**9.4.**Strategy: Encode Invariants in*Constructors***9.5.**Strategy: Encode Invariants in*Constructors***9.6.**Invariant: Ordered Pairs**9.7.**Invariant via Refined Constructors**9.8.**Invariant via Refined Constructors**9.9.**Invariant via Refined Constructors**9.10.**Refined Data: CSV Tables**9.11.**Exercise: Legal CSV Tables**9.12.**Ordered Lists**9.13.**Ordered Lists**9.14.**Recap: Invariant via Refined Constructors**9.15.**Recap: Invariant via Refined Constructors**9.16.**Plan**10.**Case Study: Optimizing Expressions**10.1.**Recall: State**10.2.**Recall: Arithmetic Expressions**10.3.**Recall: Evaluating Expressions in some`State`

**10.4.**Optimal Expressions**10.5.**Simplifying Expressions to make them Optimal**10.6.**Lets Prove that`asimp`

is "Correct"**10.7.**Another Transformation: "Normalizing"**10.8.**Specifying Normal Forms**10.9.**How to Normalize Expressions?**10.10.**Step 1: Add a Constant to an`NAExp`

**10.11.**Step 1: Why is it "correct"?**10.12.**Step 2: Add an`NAExp`

to another`NAExp`

**10.13.**Step 2: Why is it "correct"?**10.14.**Step 3: Recursively normalize and`nplus`

**10.15.**Step 3: Why is it "correct"?**10.16.**Verification with Refinement Types**10.17.**Language Integrated Verification**11.**Case Study: Vector Bounds**11.1.**Case Study: Vector Bounds**11.2.**Case Study: Vector Bounds**11.3.**Case Study: Vector Bounds**11.4.**Specifications: Pre-Conditions**11.5.**Specifications: Pre-Conditions**11.6.**Specifications: Post-Conditions**11.7.**Specifications: Post-Conditions**11.8.**Case Study: Vector Bounds**11.9.**Verification: Vector Sum**11.10.**Verification: Vector Sum**11.11.**Verification: Vector Sum**11.12.**Case Study: Vector Bounds**11.13.**Inference**11.14.**Inference: Vector Sum**11.15.**Inference: Vector Sum**11.16.**Inference: Vector Sum**11.17.**Inference: Vector Sum**11.18.**Inference: Vector Sum**11.19.**Inference: Vector Sum**11.20.**Case Study: Vector Bounds**11.21.**Collections & Higher-Order Functions**11.22.**Collections & Higher-Order Functions**11.23.**Collections & Higher-Order Functions**11.24.**Collections & Higher-Order Functions**11.25.**Collections & Higher-Order Functions**11.26.**Collections & Higher-Order Functions**11.27.**Collections & Higher-Order Functions**11.28.**Refinement Types and Collections**11.29.**Refinement Types and Collections**11.30.**Refinement Types and Collections**11.31.**Case Study: Vector Bounds**11.32.**Putting it All Together: Binary Search**11.33.**Plan**12.**AWS/ARG**12.1.**Follow Along at This URL**12.2.**Program Analysis & Verification**12.3.**Program Analysis & Verification**12.4.**Program Analysis & Verification**12.5.**Program*mer's*Analysis & Verification**12.6.**Analysis Influences Program's Design**12.7.**Analysis Influences Program's Design**12.8.**Analysis Influences Program's Design**12.9.**Analysis Influences Program's Design**12.10.**Analysis Influences Program's Design**12.11.**Program*mer's*Analysis & Verification**12.12.**Program Influences Analysis' Abilities**12.13.**Program Influences Analysis' Abilities**12.14.**Language Integrated Verification (LIVE)**12.15.**LIVE with Refinement Types**12.16.**Plan**12.17.**Program Influences Analysis' Abilities**12.18.**Language Integrated Verification**13.**Case Study: Sorting Lists**13.1.**Case Study: Sorting Lists**13.2.**Insertion Sort**13.3.**Goal: Verified Insertion Sort**13.4.**Goal: Verified Insertion Sort**13.5.**Property 1: Size**13.6.**Property 1: Size**13.7.**Goal: Verified Insertion Sort**13.8.**Property 2: Permutation**13.9.**SMT Solvers Reason About Sets**13.10.**Specifying A List's Elements**13.11.**Property 2: Permutation**13.12.**Goal: Verified Insertion Sort**13.13.**Case Study: Sorting Lists**13.14.**MergeSort: Size**13.15.**MergeSort: Permutation**13.16.**Plan**14.**Properties of Data Structures**14.1.**Properties of Data Structures**14.2.**Example: List`average`

**14.3.**Example: List`average`

**14.4.**Properties of Structures**14.5.**Properties of Structures**14.6.**Properties of Structures**14.7.**Properties of Structures**14.8.**Properties of Structures**14.9.**Properties of Structures**14.10.**Example:`map`

over Lists**14.11.**Recap: Properties of Structures**14.12.**Recap: Properties of Structures**14.13.**Recap: Properties of Structures**14.14.**Recap: Properties of Structures**14.15.**Multiple Measures are Conjoined**14.16.**Multiple Measures are Conjoined**14.17.**Plan