Towards Safe and Efficient Functional Reactive Programming

This page contains the accompanying code for my thesis "Towards Safe and Efficient Functional Reactive Programming".

Agda

The Agda code is available as a tarball, or it can be browsed as hyperlinked HTML (recommended).

Conceptual Models

• CFRP.agda
• UFRP.agda
• SigVecs.agda
• Utilities.agda
• NaryFRP.agda

N-ary FRP Library Code

• Library1.agda
• RSwitch.agda
• Library2.agda

Properties of N-ary FRP

• CausalityProps.agda
• ChangeProps.agda
• PrimProps.agda
• Loop.agda

Embedded Implementation of N-ary FRP

• Core.agda
• Primitives.agda
• Library.agda

Embedded Implementation of N-ary FRP with Feedback

• CoreD.agda
• PrimitivesD.agda
• LibraryD.agda

Now-Soon Models

• NowSoon.agda

Conceptual Model of N-ary FRP with Uninitialised Signals

• UtilitiesI.agda
• NaryFRPI.agda

Embedded Implementation of N-ary FRP with Uninitialised Signals

• CoreI.agda
• PrimitivesI.agda
• LibraryI.agda

Decoupledness Matrices

• DecMatrices.agda

Haskell

The Haskell code is available as a tarball, or the source code files can be viewed individually.

Embedded Implementation of N-ary FRP

• Core.hs
• Primitives.hs
• Library.hs

Embedded Implementation of N-ary FRP with Feedback

• CoreD.hs
• PrimitivesD.hs
• LibraryD.hs

Modules used by both Embeddings

• ArrowCombinators.lhs
• BouncingBall.hs
• Decoupled.hs
• Queue.lhs
• Time.hs
• Utilities.lhs

Last updated 16th February 2016.