We present a type system and inference algorithm for a rich subset
abstract and recursive objects, and is expressive enough to
accommodate several standard benchmarks with only minor workarounds.
The invariants enforced by the types enable an ahead-of-time
compiler to carry out optimizations typically beyond the reach of
static compilers for dynamic languages. Unlike previous inference
techniques for prototype inheritance, our algorithm uses a
combination of lower and upper bound propagation to infer types and
discover type errors in all code, including uninvoked
functions. The inference is expressed in a simple constraint
language, designed to leverage off-the-shelf fixed point solvers.
We prove soundness for both the type system and inference algorithm.
An experimental evaluation showed that the inference is powerful,
handling the aforementioned benchmarks with no manual type annotation, and
that the inferred types enable effective static compilation.
Wed 2 Nov
|15:40 - 16:05|
Sulekha KulkarniGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Xin ZhangGeorgia Tech, Mayur NaikGeorgia TechDOI
|16:05 - 16:30|
Venkatesh SrinivasanUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.DOI Pre-print
|16:30 - 16:55|
Dmytro PetrashkoEPFL, Vlad UrecheEPFL, Switzerland, Ondřej LhotákUniversity of Waterloo, Martin OderskyEPFL, SwitzerlandDOI
|16:55 - 17:20|
Satish ChandraSamsung Research America, Colin GordonDrexel University, Jean-Baptiste JeanninCarnegie Mellon University , Cole SchlesingerSamsung Research America, Manu SridharanSamsung Research America, Frank TipSamsung Research America, Young-il ChoiSamsung ElectronicsDOI Pre-print