Linear Contextual Modal Type Theory
TR-2011-151, Authors: Anders Schack-Nielsen and Carsten Schürmann
Linear Contextual Modal Type Theory
Anders Schack-Nielsen
Carsten Schürmann
December 2011
Abstract
When one implements a logical framework based on linear type theory, for example the Celf system[SNS08], one is immediately confronted with questions about their equational theory and how to deal with logic variables. In this paper, we propose linear contextual modal type theory that gives a mathematical account of the nature of logic variables. Our type theory is conservative over intuitionistic contextual modal type theory proposed by Nanevski, Pfenning, and Pientka. Our main contributions include a mechanically checked proof of soundness and a working implementation.
Technical report TR-2011-151 in IT University Technical Report Series, December 2011.
Available as PDF.