Tue 9 Jan 2018 09:00 - 09:30 at Museum B - Talks I

This talk is a gentle introduction to refinement types describing how type directed verification is automated using an SMT solver as a black box. As the refinement type checker, we use Liquid Haskell, a Haskell extension that checks that the Haskell code satisfies the refinement types, specified as Haskell comments. We can use Liquid Haskell to verify a wide range of properties ranging from the absence of infamous software bugs (e.g., heartbleed) to list laws (e.g., append is associative).

slides (plmw18.pdf)4.85MiB

Tue 9 Jan

PLMW-POPL-2018
09:00 - 10:00: PLMW - Talks I at Museum B
PLMW-POPL-201809:00 - 09:30
Talk
Niki VazouUniversity of Maryland
File Attached
PLMW-POPL-201809:30 - 10:00
Talk
File Attached