Lecture

Refinement Types: Practicality and Soundness

Description

This lecture explores the practicality and soundness of refinement types, which enhance programming language types with logical predicates for more expressive specifications. The instructor presents Liquid Haskell's refinement types, discussing their practicality, generality, expressiveness, and soundness. The lecture covers topics such as safe indexing, light properties verification, and the verification of deeper specifications like type preservation. Additionally, the lecture delves into the verification of light and deep properties using Liquid Haskell, highlighting the challenges and benefits of using refinement types in program verification.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.