Linear, Strictness and Usage Logics
David A Wright
Department of Computer Science,
The University of Tasmania,
Hobart 7001, Australia.
This paper introduces a new framework for intensional logics that
provides a consistent syntax for specifying and reasoning about
these logics. Important properties such as the proof
normalisation property can be proved in a modular way in the
framework, thus reducing the work required to establish these
properties for new logics.
The generality and practicality of the system will be demonstrated by
encoding some well known intensional logics:
Linear Logic, Strictness Logic and Usage Logic(s).
The encodings reveal new insights into the relationship between
Conference Home Page