Repository files navigation

This package encodes a version of intuitionistic linear logic on top of linear Haskell, using a variation of thetechnique described by Michael Shulman inLinear Logic for Constructive Mathematics. Embedding a larger linear logic into the simple linear logic available to us in Linear Haskell means we are able torecover the full suite of linear unitors, not just two of them, meaning we model linear logic, rather than affine logic.

The central idea is to track for each type not just its type of proofs, but also its type of refutations.

Contributions and bug reports are welcome!

Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.

-Edward Kmett