Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

A simple development of linear logic in Coq.

branch: master

Fetching latest commit…

Octocat-spinner-32-eaf2f5

Cannot retrieve the latest commit at this time

Octocat-spinner-32 BlocksWorldExample1.v
Octocat-spinner-32 Context.v
Octocat-spinner-32 LinLog.v
Octocat-spinner-32 LinProp.v
Octocat-spinner-32 Makefile
Octocat-spinner-32 PermutationHelpers.v
Octocat-spinner-32 README.md
Octocat-spinner-32 Sig.v
Octocat-spinner-32 _CoqProject
README.md

A simple Coq development of linear logic. The library is inspired by the paper, J. Power and C. Webster, "Working with linear logic in coq," in The 12th International Conference on Theorem Proving in Higher Order Logics, 1999.

This particular devlopment is based more immediately on that used in A. Cowley and C.J. Taylor, "Stream-oriented robotics programming: The design of roshask," in Proceedings of the IEEE/RJS International Conference on Intelligent Robots and Systems (IROS), 2011. pdf

Tested with Coq 8.4.

An example command to build the documentation,

coqdoc --no-lib-name -d doc *.v --utf8 --no-index

(this requires that the directory doc exists).

Something went wrong with that request. Please try again.