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.

Conference Day
Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South
Chair(s): Tiark RompfPurdue & Oracle Labs
14:20
25m
Talk
Principal Type Inference for GADTs
Research Papers
Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University
Media Attached
14:45
25m
Talk
Abstracting Gradual Typing
Research Papers
Ronald GarciaUniversity of British Columbia, Alison M. Clark, √Čric TanterUniversity of Chile, Chile
Link to publication Media Attached
15:10
25m
Talk
The Gradualizer: a methodology and algorithm for generating gradual type systems
Research Papers
Matteo CiminiIndiana University, Jeremy G. SiekIndiana University
Media Attached
15:35
25m
Talk
Is Sound Gradual Typing Dead?
Research Papers
Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University
Pre-print Media Attached File Attached