The home of the source files accompanying the MWSCAS 2020 submission "On Applications of Dependent Types to Parameterised Digital Signal Processing Circuits". We present an experimental circuit simulation library for Idrs, a lovely functional language with dependent types.
The main examples are:
- An FIR with minimal bit growth (both signed and unsigned)
- A CIC filter with Hogenauer's register pruning strategy
Idris sources and a Nix shell description are in src/
, and paper contents to
be linked on publication.