Language Based Verification Tools for Functional Programs

Summary

Tis report summarizes the program and the outcomes of Dagstuhl Seminar 16131 "Language Based Verification Tools for Functional Programs", organized by:

• Marco Gaboardi, School of Computing, University of Dundee, UK
• Suresh Jagannathan, Purdue University, USA
• Ranjit Jhala, University of California, San Diego, USA
• Stephanie Weirich, University of Pennsylvania, USA.

The web, multi-core and "big-data" revolutions have been largely built on higher-order programming constructs pioneered in the Functional Programming community. Despite the increasing importance of such programs, there are relatively few tools that are focussed on ensuring that functional programs possess crucial correctness properties. While language based verification for imperative and first-order programs has been studied for decades yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, and Model Checking. It is only relatively recently, that researchers have proposed language based verification tools {e.g. advanced type systems, contract systems, model checking and higher-order program analyses for functional and higher-order programs.

We organised this seminar to bring together the different schools of researchers interested in software reliability, namely, the designers and implementers of functional programming languages, and experts in software verification, in order create a larger community of researchers focused on this important goal, to let us compare the strengths and limitations of different approaches, to find ways to unite both intellectually, and via tools the complementary advantages of different techniques, and to devise challenging open problems and application areas where verification may be most effective.To this end, the seminar comprised a program of 30 talks from the leading experts on the above topics, and breakout sessions on:

1. Integrating formal methods tools in the curriculum
2. Hands on Tool Tutorials
3. User Interaction
4. Types and Effects