28. März – 01. April 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)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 6, Issue 3 Dagstuhl Report
Gemeinsame Dokumente
Dagstuhl's Impact: Dokumente verfügbar
Programm des Dagstuhl-Seminars [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 der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.