Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 13:30 - 13:55 at Noh Theater - Session 6 Chair(s): Johan Jeuring

Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend the above procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message.

Tue 20 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

13:30 - 14:45
Session 6Research Papers at Noh Theater
Chair(s): Johan Jeuring Utrecht University
13:30
25m
Talk
Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)
Research Papers
Eric Seidel University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA, Westley Weimer University of Virginia, USA
DOI
13:55
25m
Talk
Automatically Disproving Fair Termination of Higher-Order Functional Programs
Research Papers
Keiichi Watanabe University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan
DOI
14:20
25m
Talk
Higher-Order Ghost State
Research Papers
Ralf Jung MPI-SWS, Germany, Robbert Krebbers Aarhus University, Denmark, Lars Birkedal Aarhus University, Denmark, Derek Dreyer MPI-SWS, Germany
DOI