Working with Linear Logic in Coq
In this paper we describe the encoding of linear logic in the Coq
system, a proof assistant for higher-order logic. This process
involved encoding a suitable consequence relation, the relevant
operators, and some auxiliary theorems and tactics. The encoding
allows us to state and prove theorems in linear logic, and we
demonstrate its use through two examples: a simple blocks world
scenario, and the Towers of Hanoi problem.
The paper describing this work is:
Working with Linear Logic in Coq,
James Power and Caroline Webster,
12th International Conference on Theorem Proving in Higher Order Logics (Work-in-progress paper), University of Nice, France, September 14-17, 1999.
There were also some slides
presented as the work-in-progress session at TPHOLs '99.
- The basic source code for linear logic is in the files moreLists.v, ILL.v and extraLL.v
- The blocks world example is blocks.v
- The Towers of Hanoi example is in discs.v, auxHanoi.v and hanoi.v
- All of the above as a .tar.gz file
Some related papers are:
- David Gray, Geoff Hamilton, James Power and David Sinclair,
A Specification of TCP/IP using Mixed Intuitionistic Linear
Logic (Extended Abstract),
2nd Joint Workshop on Formal Specification of Computer-Based Systems,
Washington DC, USA, 20 April, 2001.
David Sinclair, James Power, Paul Gibson, David Gray, and
Specifying and Verifying IP with Linear Logic,
International Workshop on Distributed Systems Validation and
Taipei , Taiwan, ROC, 10 April, 2000.
- David Gray, Geoff Hamilton, David Sinclair, Paul Gibson and James Power,
Four Logics and a Protocol
3rd. Irish Workshop in Formal Methods,
National University of Ireland, Galway, Ireland, 1-2 July, 1999.
Revised: 19th May 2001