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 2nd July 2024.

Valid XHTML 1.0 Strict I'm a Haskeller