Fri 22 Jun 2018 17:00 - 17:25 at Grand Ballroom CD - Types Chair(s): Kathleen Fisher

Type systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structure. As a result, type errors can reference terms the programmers did not write (and even constructs they do not know), baffling them. The language developer must also manually construct type rules for the sugars, to give a typed account of the surface language. We address these problems by presenting a process for automatically reconstructing type rules for the surface language using rules for the core. We have implemented this theory, and show several interesting case studies.

Fri 22 Jun

Displayed time zone: Eastern Time (US & Canada) change

16:10 - 17:25
TypesPLDI Research Papers at Grand Ballroom CD
Chair(s): Kathleen Fisher Tufts University
16:10
25m
Talk
Guarded Impredicative Polymorphism
PLDI Research Papers
Alejandro Serrano Utrecht University, Jurriaan Hage Utrecht University, Dimitrios Vytiniotis Microsoft Research, Cambridge, Simon Peyton Jones Microsoft Research
Media Attached
16:35
25m
Talk
Typed Closure Conversion for the Calculus of Constructions
PLDI Research Papers
William J. Bowman Northeastern University, USA, Amal Ahmed Northeastern University, USA
Media Attached
17:00
25m
Talk
Inferring Type Rules for Syntactic Sugar
PLDI Research Papers
Justin Pombrio Brown University, USA, Shriram Krishnamurthi Brown University, USA
Media Attached