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

This extended abstract presents a the formally verification a subset of SPIRAL, an efficient code generation system for digital signal processing algorithms and related computations. SPIRAL represents algorithms for linear transforms as sparse matrix factorizations using a domain specific language called the Signal Processing Language (SPL). To produce an algorithm, SPL expressions representing a signal transform factorization are rewritten through repeated application of factorization and matrix identities. SPL expressions representing completely factorized transforms can be compiled to a target language. A subset of SPIRAL’s algorithm space as well as an SPL compiler targeting a simple imperative language with arrays and values from a commutative ring, IMP+V, are verified using the Coq proof assistant.

Abstract (coqpl21-final64.pdf)554KiB

Tue 19 Jan
Times are displayed in 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