u/TechnoEmpressin r/haskell • Recommends
Niki Vazou: Liquid Haskell: Verification with Refinement Types (MuniHac 2024)
0:00 / 0:00
#liquidhaskell#refinementtypes
MuniHac 2024 - So, Oct. 13 - Niki Vazou: Liquid Haskell: Verification with Refinement Types
TNG Technology Consulting GmbH
5K subscribers • 17 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Niki Vazou
Advanced. Deep dive for people who know the field.
578 views2 years ago1 recommendation
Programming languagesComputer scienceHaskellFormal methods and verificationComputation and complexity
Niki Vazou demonstrates how to use Liquid Haskell's refinement type checker to verify properties of Haskell programs.
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.Why it's here
1 person recommends thisWhat people say. Recommended as an excellent introduction to program verification using Liquid Haskell.