DepSec: Static Information-Flow Control in Idris
This repository contains DepSec, a dependently typed library for static information-flow control in Idris.
DepSec has been built and tested using
- Idris 1.3.1.
Copy this package and run
$ idris --install depsec.ipkg
To use it in your program, run Idris with
$ idris -p depsec yourprogram.idr
DepSec- core library, together with declassification primitives
Examples- case studies and examples from the paper