Linear, Strictness and Usage Logics

David A Wright
Department of Computer Science, The University of Tasmania, Hobart 7001, Australia.
D.A.Wright@cs.utas.edu.au

Abstract

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 these logics.

Conference Home Page