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: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00
Compilation and ConcurrencyResearch Papers at Stifel Theatre
Chair(s): Heather MillerCarnegie Mellon University
10:30
22m
Talk
Competitive Parallelism: Getting Your Priorities Right
Research Papers
Stefan K. Muller, Umut A. AcarCarnegie Mellon University, Robert Harper
DOI
10:52
22m
Talk
Static Interpretation of Higher-Order Modules in Futhark: Functional GPU Programming in the Large
Research Papers
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
11:15
22m
Talk
Finitary Polymorphism for Optimizing Type-Directed Compilation
Research Papers
Atsushi OhoriTohoku University, Japan, Katsuhiro UenoTohoku University, Hisayuki MimaTohoku University
DOI
11:37
22m
Talk
Fault Tolerant Functional Reactive Programming (Functional Pearl)
Research Papers
Ivan PerezNational Institute of Aerospace, USA
DOI