/Idris_dsp_motivation

Primary LanguageIdrisBSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

On Applications of Dependent Types to Parameterised Digital Signal Processing Circuits

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:

  1. An FIR with minimal bit growth (both signed and unsigned)
  2. 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.

License

BSD 3-clause