Proofs

Selected formal developments:

• W-Calculus, verified semantics for a DSP-oriented synchronous programming language.

• mech.v, a formalization project for mechanism design.

• VerDILog, an incremental Datalog engine with support for regular queries.

• ssrbit, a library for bit sequences and bit sets.

• C-DFT, a constructive formalization of the Discrete Fourier Transform and some associated properties.