Implementing Substructural Logical Frameworks
Anders Schack-Nielsen · 2011
A key component in proof assistant software is the meta-language used to encode the objects that are being reasoned about. Such a meta-language is called a logical framework. Several different logical frameworks exist; some only provide the most basic encoding of abstract syntax data, while others support powerful representation methodologies and concepts such as judgments-as-types and higher-order abstract syntax, e.g. the logical framework LF. The direct support for high-level concepts in the logical framework allows for rapid prototyping of new logics, type systems, and semantics. It also eases the development of theorems when the key concepts are directly supported. A concept, which is becoming increasingly important, is resources, but so far resources have not been supported very well by existing logical frameworks. In this thesis I develop the theoretical infrastructure required to implement — and give an implementation of — a new logical framework that extends LF with the concepts of both linear resources, which must be used exactly once, and affine resources, which can be used at most once.