An experience report on writing usable DSLs in Coq (CoqPL 2021 - The Seventh International Workshop on Coq for Programming Languages)

Write a Blog >>

Sun 17 - Fri 22 January 2021 Online

Who

Clément Pit-Claudel, Thomas Bourgeat

Track

CoqPL 2021

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 19 Jan 2021 18:15 - 18:30 at CoqPL - Contributed Talks

Abstract

Features added to Coq over the last 5 years have made it possible to create drastically more usable domain-specific languages (DSLs). We report on our experience building and using a hardware-description language embedded within Coq, highlighting how recent Coq improvements make it possible to solve longstanding pain points with Coq DSLs.

File attachments

Abstract (coqpl21-final99.pdf)	338KiB

Clément Pit-Claudel

Massachusetts Institute of Technology, USA

Thomas Bourgeat

MIT CSAIL