Verified Functional Programming: Nicolas Voirol public PhD thesis defense

This lecture covers the concept of verified functional programming, emphasizing the importance of formal verification in software development to prevent catastrophic bugs. It explores the challenges of verifying programs, the benefits of functional programming, and the use of SMT solvers for counterexample finding. The lecture delves into type checking, bidirectional type checking, and the encoding of Scala language features. It also discusses automation, improvements in program verification, and the theoretical results of counterexample finding. The presentation concludes with the application of dependent types, Scala program transformations, and the enforcement of laws in program design.