[POPLmark] Meta-meta-comment

[David Walker]

There have been a couple assertions that LF can represent linear logic.  It
can be done as Karl and Bob suggested, but it takes an "order of magnitude"
more work to start investigating metatheoretic properties of linear logic
than it does for ordinary intuitionistic logic, for instance.  Frank wrote a
nice paper some time ago that shows it is possible to represent linear logic
in LF.  More importantly, however, he shows it becomes a lot easier when you
add a couple of simple linear connectives to the framework itself.  This
helped motivate Linear LF.  If you're interested in how this works, I
suggest:

Frank Pfenning. Structural cut elimination in linear logic. Technical Report
CMU-CS-94-222, Department of Computer Science, Carnegie Mellon University,
December 1994.

Dave