This Dagstuhl Seminar is motivated by two converging trends in computing. First, the increasing reliance on software has led to an increased interest in seeking formal, reliable means of ensuring that programs possess crucial correctness properties. Second, the rise of the web, multicore, and “big data” has led to a dramatic increase in higher-order functional languages that are seeing a dramatic uptick in adoption, either directly (e.g. Scala, Haskell, F#, Clojure), or via the incorporation of functional features - first-class functions, parametric polymorphism, immutability, algebraic datatypes and so on - in imperative languages, both legacy (e.g. Java, C++) and emerging (e.g. Python, Swift, Rust).

In theory, functional programs are ideal for language based verification. They offer a rich semantic structure that allows the description of different correctness properties in a natural way. They provide a powerful abstraction mechanism – first class functions – that is helpful to construct programs and verify correctness properties in a modular way. They emphasize programming without pervasive mutation and side-effects which promotes mathematical (e.g. algebraic) reasoning. In practice, however, while the research community has studied the problem of language based verification for imperative and first-order programs for decades – yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, Model Checking, and Separation Logic and so on – it is only relatively recently, that proposals have emerged for language based verification tools for functional and higher-order programs.

These techniques include advanced type systems, contract systems, model checking and program analyses specially tailored to exploit the structure of functional languages. These proposals are from groups based in diverse research communities, attacking the problem from different angles, yielding techniques with complementary strengths. All the above methods let the programmer specify fine-grained properties that the program should satisfy, and then verify that in a given implementation, data and program components are used in a way that meets the specification. However, they differ widely in trade-offs made between the expressiveness of the specifications and automation of the verification. At one end of the spectrum, dependent type systems are extremely expressive, but require the programmer to provide proofs, while at the other end program analyses are limited to finite state specifications but are fully automatic.

The overall goal of this seminar is to bring together researchers working in all related areas so that we may

• compare the strengths and limitations of the different approaches,
• discuss ways to unify the complementary advantages of different techniques, both conceptually and in tools,
• share challenging open problems and application areas where verification may be most effective,
• identify novel ways of using verification techniques for other software engineering tasks such as code search or synthesis, and
• improve the pedagogy and hence adoption of such techniques.

In other words, the aim of this Dagstuhl Seminar is to catalyze the creation of a larger community of researchers working on the above topics, thereby accelerating the research and adoption of language based verification for functional programs.

• Andreas Martin Abel (Chalmers UT - Göteborg, SE) [dblp]
• Amal Ahmed (Northeastern University - Boston, US) [dblp]
• Andrew W. Appel (Princeton University, US) [dblp]
• Lennart Augustsson (Standard Chartered Bank - London, GB) [dblp]
• Edwin Brady (University of St. Andrews, GB) [dblp]
• Iavor Diatchki (Galois - Portland, US) [dblp]
• Richard A. Eisenberg (University of Pennsylvania - Philadelphia, US) [dblp]
• Jean-Christophe Filliâtre (CNRS & University Paris Sud, FR) [dblp]
• Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
• Marco Gaboardi (SUNY - Buffalo, US) [dblp]
• Deepak Garg (MPI-SWS - Saarbrücken, DE) [dblp]
• Michael Greenberg (Pomona College - Claremont, US) [dblp]
• Reiner Hähnle (TU Darmstadt, DE) [dblp]
• Catalin Hritcu (INRIA - Paris, FR) [dblp]
• Suresh Jagannathan (Purdue University - West Lafayette, US) [dblp]
• Ranjit Jhala (University of California - San Diego, US) [dblp]
• Gowtham Kaki (Purdue University - West Lafayette, US) [dblp]
• Gabriele Keller (UNSW - Sydney, AU) [dblp]
• Naoki Kobayashi (University of Tokyo, JP) [dblp]
• Ekaterina Komendantskaya (University of Dundee, GB) [dblp]
• Martin Lange (Universität Kassel, DE) [dblp]
• K. Rustan M. Leino (Microsoft Corporation - Redmond, US) [dblp]
• Conor McBride (University of Strathclyde - Glasgow, GB) [dblp]
• Jan Midtgaard (Technical University of Denmark - Lyngby, DK) [dblp]
• Chih-Hao Luke Ong (University of Oxford, GB) [dblp]
• Dominic Orchard (University of Cambridge, GB) [dblp]
• Brigitte Pientka (McGill University - Montreal, CA) [dblp]
• Ruzica Piskac (Yale University, US) [dblp]
• Nadia Polikarpova (MIT - Cambridge, US) [dblp]
• Scott Smith (Johns Hopkins University - Baltimore, US) [dblp]
• Matthieu Sozeau (University Paris-Diderot, FR) [dblp]
• Wouter Swierstra (Utrecht University, NL) [dblp]
• Tachio Terauchi (JAIST - Ishikawa, JP) [dblp]
• Sam Tobin-Hochstadt (Indiana University - Bloomington, US) [dblp]
• Hiroshi Unno (University of Tsukuba, JP) [dblp]
• David Van Horn (University of Maryland - College Park, US) [dblp]
• Niki Vazou (University of California - San Diego, US) [dblp]
• Stephanie Weirich (University of Pennsylvania - Philadelphia, US) [dblp]
• Nobuko Yoshida (Imperial College London, GB) [dblp]