Safe Functional Reactive Programming though Dependent Types

Accompanying code for the paper Safe Functional Programming though Dependent Types can be accessed here. You can either download the Agda source files, or browse them as html. There is also a related Haskell implementation that encodes decoupledness using Type Families. This implementation diverges somewhat from the paper, but provides greater functionality.

There are three Agda versions available:

Implementation Without Uninitialised Signals (icfp09)

Full Implementation (icfp09Full)

Basic Implementation without "type-in-type" Option (icfp09Set1)

Last updated 13th May 2017.

Valid XHTML 1.0 Strict I'm a Haskeller