Skip to content

They see me rollin'. They're Heyting. -- Chamillionaire, 2005

License

Notifications You must be signed in to change notification settings

ekmett/linear-logic

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

48 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

linear-logic

Hackage Build Status

This package encodes a version of intuitionistic linear logic on top of linear Haskell, using a variation of the technique described by Michael Shulman in Linear Logic for Constructive Mathematics. Embedding a larger linear logic into the simple linear logic available to us in Linear Haskell means we are able to recover 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.

Contact Information

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

About

They see me rollin'. They're Heyting. -- Chamillionaire, 2005

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published