Write a Blog >>
Thu 21 Jan 2016 14:20 - 14:45 at Grand Bay South - Track 2: Types, Generally or Gradually Chair(s): Tiark Rompf

We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our approach is that can detect a wide range of runtime errors that are missed by previous approaches.

Our method is based on the idea to represent type refinements in pattern-matching branches by choice types, which facilitate a separation of the typing and reconciliation phases and thus support for case expressions. This idea is formalized in a type system, which is both sound and a conservative extension of the classical Hindley-Milner system. We present the results of an empirical evaluation that compares our algorithm with previous approaches.

Thu 21 Jan

14:20 - 16:00: Research Papers - Track 2: Types, Generally or Gradually at Grand Bay South
Chair(s): Tiark RompfPurdue & Oracle Labs
POPL-2016-papers145338240000014:20 - 14:45
Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University
Media Attached
POPL-2016-papers145338390000014:45 - 15:10
Ronald GarciaUniversity of British Columbia, Alison M. Clark, √Čric TanterUniversity of Chile, Chile
Link to publication Media Attached
POPL-2016-papers145338540000015:10 - 15:35
Matteo CiminiIndiana University, Jeremy G. SiekIndiana University
Media Attached
POPL-2016-papers145338690000015:35 - 16:00
Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University
Pre-print Media Attached File Attached