Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 18:15 - 18:30 at CoqPL - Contributed Talks

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.

Abstract (coqpl21-final99.pdf)338KiB

Conference Day
Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:45
Contributed TalksCoqPL at CoqPL
18:00
15m
Talk
Verification of Algorithm and Code Generation for Signal Transforms
CoqPL
Patrick BrinichDrexel University, Jeremy JohnsonDrexel University, USA
File Attached
18:15
15m
Talk
An experience report on writing usable DSLs in Coq
CoqPL
Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Thomas BourgeatMIT CSAIL
File Attached
18:30
15m
Break
Break
CoqPL