A self-contained implementation of Mike Shulman's “meaning explanation” for his variant of linear logic, written for the Agda proof assistant.
See the n-category cafe article for the meaning explanations, and arXiv for the paper on linear triposes.
The files should typecheck with Agda version 2.5.1 and above. You will need a reasonably recent version of the relevant parts of the standard library; failing that, you will have to supply the definitions of conjunction, disjunction and equality manually.
- Create a fork!
- Create your feature branch:
git checkout -b my-new-feature - Commit your changes:
git commit -am 'Add some feature' - Push to the branch:
git push origin my-new-feature - Submit a pull request.
- Zoltan A. Kocsis - University of Manchester
- Shimin Guo