Paralocks in the Haskell type system

Potential supervisors: 

Information flow control can be achieved through static (i.e. compile time) or dynamic (i.e. runtime) enforcement.
Static enforcement has many benefits; errors are caught before deployment, and typically no runtime overhead is added.
However, to achieve static control, existing solutions typically implement a full type-checker, a practice that is rather

As an interesting alternative, seclib [1,2] implements static information flow control in GHC Haskell by
cleverly utilizing the type system. No separate type-checker is needed, and the whole solution can be presented as
a library, an EDSL. The drawback with SecIO, however, is that the policies that can be expressed at the type level
are very basic - too basic for practical use.

Paralocks [3] is a rich language for expressing information flow policies. It (or variants thereof) has been used 
previously in Paragon [4,5], which uses a full type-checker solution; and in SLIO [6] which performs dynamic enforcement
in Haskell.

This project would investigate the feasibility of implementing an enforcement of Paralocks (or a variant thereof)
using the SecIO approach, by implementing the enforcement mechanism using the advanced type system mechanisms found in GHC Haskell.