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 Times are displayed in time zone: Eastern Time (US & Canada) change
Fri 22 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change
16:10 - 17:25: TypesPLDI Research Papers at Grand Ballroom CD Chair(s): Kathleen FisherTufts University | |||
16:10 - 16:35 Talk | Guarded Impredicative Polymorphism PLDI Research Papers Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University, Dimitrios VytiniotisMicrosoft Research, Cambridge, Simon Peyton JonesMicrosoft Research Media Attached | ||
16:35 - 17:00 Talk | Typed Closure Conversion for the Calculus of Constructions PLDI Research Papers Media Attached | ||
17:00 - 17:25 Talk | Inferring Type Rules for Syntactic Sugar PLDI Research Papers Media Attached |