March 28 – April 1 , 2016, Dagstuhl Seminar 16131

Language Based Verification Tools for Functional Programs


Marco Gaboardi (SUNY – Buffalo, US)
Suresh Jagannathan (Purdue University – West Lafayette, US)
Ranjit Jhala (University of California – San Diego, US)
Stephanie Weirich (University of Pennsylvania – Philadelphia, US)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 6, Issue 3 Dagstuhl Report
Aims & Scope
List of Participants
Dagstuhl's Impact: Documents available
Dagstuhl Seminar Schedule [pdf]


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
Summary text license
  Creative Commons BY 3.0 Unported license
  Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich


  • Programming Languages / Compiler
  • Verification / Logic


  • Verification
  • Dependent Types
  • Refinement Types
  • SMT Solvers
  • Higher-Order Program Analysis


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.