Abstract

There has been much interest in the foundations of Linear Logic, with many detailed results concerning its semantics and complexity of proof search. Recently there have been some attempts at using Linear Logic as a basis for specification and verification. In this talk I will survey some of these attempts, and show how an implementation of Linear Logic in the Isabelle theorem prover can provide an appropriate environment for such applications, by supplying a well-developed interactive environment and `rapid prototyping' of logics.