BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:PL Seminar: Finding Minimum Type Error Sources
DTSTART:20140528T140000
DTEND:20140528T150000
DTSTAMP:20260407T045643Z
UID:14e21f323d695427555c621681dbe27a79d307f48b36b7c28402eb89
CATEGORIES:Conferences - Seminars
DESCRIPTION:Zvonimir Pavlinovic (research intern with UC\nBerkeley Securit
 y Group)\nAutomatic type inference is a popular feature of functional prog
 ramming\nlanguages. If a program cannot be typed\, the\ncompiler typically
  reports a single program location in its error\nmessage. This location is
  the point where the type inference\nfailed\, but not necessarily the actu
 al source of the error. Other\npotential error sources are not even consid
 ered. Hence\, the\ncompiler often misses the true error source\, which inc
 reases debugging\ntime for the programmer. In this paper\, we present\na g
 eneral framework for automatic localization of type errors. Our\nalgorithm
  finds all minimum error sources\, where the exact\ndefinition of minimum 
 is given in terms of a compiler-specific ranking\ncriterion. Compilers can
  use minimum error sources to\nproduce more meaningful error reports\, and
  for automatic error\ncorrection. Our approach works by reducing type infe
 rence to\nconstraint satisfaction. We then formulate the problem of comput
 ing\nminimum error sources in terms of weighted maximum\nsatisfiability mo
 dulo theories (MaxSMT). Ranking criteria are\nincorporated by assigning we
 ights to typing constraints. The\nreduction to MaxSMT allows us to built o
 n SMT solvers to support rich\ntype systems. We have implemented an instan
 ce\nof our framework targeted at Hindley-Milner type systems. We have\neva
 luated our implementation on existing OCaml\nbenchmarks for type error loc
 alization and showed that our approach can\nfind minimum error sources sub
 ject to useful\nranking criteria.
LOCATION:INR 113 http://plan.epfl.ch/?room=INR%20113
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR