Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Thu 18 Jun 2020 14:40 - 15:00 at PLDI Research Papers live stream - Language Design I Chair(s): Adrian Sampson

The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits.
Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design.
In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the \emph{scheduling} decisions that determine performance.
Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies.
Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits.
We argue that most of the extra circuitry required for dynamic analysis can be eliminated by compile-time BSV-style static analysis.

Thu 18 Jun

Displayed time zone: Pacific Time (US & Canada) change

14:20 - 15:40
14:20
20m
Talk
Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
PLDI Research Papers
Benjamin Bichsel ETH Zurich, Switzerland, Maximilian Baader ETH Zurich, Switzerland, Timon Gehr ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland
14:40
20m
Talk
The Essence of Bluespec: A Core Language for Rule-Based Hardware Design
PLDI Research Papers
Thomas Bourgeat Massachusetts Institute of Technology, USA, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology, Arvind Massachusetts Institute of Technology, USA
15:00
20m
Talk
LLHD: A Multi-level Intermediate Representation for Hardware Description Languages
PLDI Research Papers
Fabian Schuiki ETH Zurich, Switzerland, Andreas Kurth ETH Zurich, Switzerland, Tobias Grosser ETH Zurich, Switzerland, Luca Benini ETH Zurich, Switzerland
Link to publication Pre-print
15:20
20m
Talk
On the Principles of Differentiable Quantum Programming Languages
PLDI Research Papers
Shaopeng Zhu University of Maryland, USA, Shih-Han Hung University of Maryland, USA, Shouvanik Chakrabarti University of Maryland, USA, Xiaodi Wu University of Maryland, USA