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
Times are displayed in time zone: Pacific Time (US & Canada) change

14:20 - 15:40: Language Design IPLDI Research Papers at PLDI Research Papers live stream
Chair(s): Adrian SampsonCornell University, USA

YouTube lightning session video

14:20 - 14:40
Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
PLDI Research Papers
Benjamin BichselETH Zurich, Switzerland, Maximilian BaaderETH Zurich, Switzerland, Timon GehrETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
14:40 - 15:00
The Essence of Bluespec: A Core Language for Rule-Based Hardware Design
PLDI Research Papers
Thomas BourgeatMassachusetts Institute of Technology, USA, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology, ArvindMassachusetts Institute of Technology, USA
15:00 - 15:20
LLHD: A Multi-level Intermediate Representation for Hardware Description Languages
PLDI Research Papers
Fabian SchuikiETH Zurich, Switzerland, Andreas KurthETH Zurich, Switzerland, Tobias GrosserETH Zurich, Switzerland, Luca BeniniETH Zurich, Switzerland
Link to publication Pre-print
15:20 - 15:40
On the Principles of Differentiable Quantum Programming Languages
PLDI Research Papers
Shaopeng ZhuUniversity of Maryland, USA, Shih-Han HungUniversity of Maryland, USA, Shouvanik ChakrabartiUniversity of Maryland, USA, Xiaodi WuUniversity of Maryland, USA