Haskell Utrecht Meetup

The next Haskell Utrecht Meetup will be on April 23rd.

We will be in at the Channable office again -- mark your calendars because this is one Meetup that you won't want to miss!

We are thrilled to announce we will have Niki Vazou and Simon Peyton Jones give a talk.

Agenda
19:00: Doors open
19:30: Welcome
19:35: Liquid Haskell: Verification with Refinement Types, Niki Vazou
20:15: Break
21:00: Triemaps that match, Simon Peyton Jones
21:40: Drinks

Abstracts
== Liquid Haskell: Verification with Refinement Types, Niki Vazou

Refinement types decorate the types of a programming language with logical predicates to allow more expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories and allowed automatic “light” verification, for example properties like non-division by zero or in-bound indexing. Verification of such light properties though requires “deeper” specifications, for example “is append associative?” In this talk, we will interactively see how to use the refinement type checker of Liquid Haskell to verify Haskell programs.

== Triemaps that match, Simon Peyton Jones

In applications such as compilers and theorem provers, we often want to match a target term against multiple patterns (representing rewrite rules or axioms) simultaneously. Efficient matching of this kind is well studied in the theorem prover community, but much less so in the context of statically typed functional programming. Doing so yields an interesting new viewpoint — and a practically useful design pattern, with good runtime performance.