log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
Liquid Types for Haskell
Niki Vazou - UCSD
4172 A.V. Williams Building (AVW)
Thursday, November 3, 2016, 1:00-2:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

Haskell's type system allows developers to specify and verify a variety of program properties at compile time. However, many properties are impossible, or at the very least, cumbersome to encode within Haskell’s type system. Liquid types enable the specification and verification of value-dependent properties by extending Haskell’s type system with logical predicates drawn from efficiently decidable logics.

In this talk, we present an overview of LiquidHaskell, a liquid type checker for Haskell. In particular, we will describe the kinds of properties that can be checked, ranging from generic requirements like totality and termination, to application specific concerns like memory safety and correctness invariants.
Bio

Niki Vazou is currently finishing her PhD at UCSD and will be starting at Maryland as a Basili Postdoctoral Scholar in the Spring.

This talk is organized by David Van Horn