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.
Some related papers are:
James Power
Revised: 19^{th} May 2001
Contact: James.Power@may.ie