Explore refinement types and their applications in light to deep verification in this 46-minute conference talk from ACM SIGPLAN's PLMW@POPL'24. Delve into how refinement types enhance programming language types with logical predicates for more expressive specifications. Discover the evolution from automatic "light" verification of properties like non-division by zero to "deeper" specifications such as append associativity and language type preservation. Follow along as Niki Vazou provides an overview of refinement types, using Liquid Haskell as a prototype implementation to demonstrate various examples spanning both light and deep refinement type-based verification techniques.