Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
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.