Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Tue 25 Sep 2018 11:15 - 11:37 at Stifel Theatre - Compilation and Concurrency Chair(s): Heather Miller

We develop a type-theoretical method for optimizing type directed compilation of polymorphic languages, implement the method in a full-scale compiler of Standard ML extended with several advanced features that require type-passing operational semantics, and report its effectiveness through performance evaluation. For this purpose, we first define a predicative second-order lambda calculus with finitary polymorphism, where each type abstraction is explicitly constrained to a finite type universe, and establishes the type soundness with respect to a type-passing operational semantics. Different from a calculus with stratified type universes, type universes of the calculus are terms that represent the exact finite set of instance types. We then develop a universe reconstruction algorithm that takes a term of the standard second-order lambda calculus, checks if the term is typable with finitary polymorphism, and, if typable, constructs a term in the calculus of finitary polymorphism. Based on these results, we present a type-based optimization method for polymorphic functions. Since our formalism is based on the second-order lambda calculus, it can be used to optimize various polymorphic languages. We implement the optimization method for natural (tag-free) data representation and record polymorphism, and evaluate its effectiveness through benchmarks. The evaluation shows that 84% of type passing abstractions are eliminated, and achieves the average of 11% speed-up of compiled code.

Tue 25 Sep
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

10:30 - 12:00: Research Papers - Compilation and Concurrency at Stifel Theatre
Chair(s): Heather MillerCarnegie Mellon University
icfp-2018-papers10:30 - 10:52
Stefan K. Muller, Umut A. AcarCarnegie Mellon University, Robert Harper
icfp-2018-papers10:52 - 11:15
Martin ElsmanUniversity of Copenhagen, Denmark, Troels HenriksenUniversity of Copenhagen, Denmark, Danil AnnenkovDepartment of Computer Science, University of Copenhagen, Cosmin OanceaUniversity of Copenhagen, Denmark
Link to publication DOI
icfp-2018-papers11:15 - 11:37
Atsushi OhoriTohoku University, Japan, Katsuhiro UenoTohoku University, Hisayuki MimaTohoku University
icfp-2018-papers11:37 - 12:00
Ivan PerezNational Institute of Aerospace, USA