Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Sat 29 Sep 2018 09:00 - 10:00 at New York Central - Morning Session 1 Chair(s): Kei Davis

In this paper, we present HELIX, a formally verified operator language and rewriting engine for generation of high-performance implementation for a variety of linear algebra algorithms. Based on the existing SPIRAL system, HELIX adds the rigor of formal verification of its correctness using Coq proof assistant. It formally defines two domain-specific languages: HCOL, which represents a computation data flow and Sigma-HCOL, which extends HCOL with iterative computations. A framework for automatically proving \textit{semantic preservation} of expression rewriting for both languages is presented. The structural properties of the dataflow graph which allow efficient compilation are formalized, and a monadic approach to tracking them and to reasoning about \textit{structural correctness} of Sigma-HCOL expressions is presented.

Sat 29 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:45 - 10:00
Morning Session 1FHPC at New York Central
Chair(s): Kei Davis Los Alamos National Laboratory
08:45
15m
Day opening
Welcome and Introductions
FHPC
C: Kei Davis Los Alamos National Laboratory, C: Mike Rainey
09:00
60m
Talk
HELIX: A Case Study of a Formal Verification of High Performance Program Generation
FHPC
A: Vadim Zaliva Carnegie Mellon University, USA, A: Franz Franchetti Carnegie Mellon University, USA
DOI