Working with Linear Logic in Coq
James F. Power, Caroline E. Webster · Maynooth University ePrints and eTheses Archive (Maynooth University) · 1999
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.