@book{e87d09dd2a8049378ff0d295fcdfab4e,
title = "Linear contextual modal type theory",
abstract = "Abstract. When one implements a logical framework based on linear type theory, for example the Celf system [?], one is immediately con- fronted 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.",
keywords = "Linear Type Theory, Logical Framework, Contextual Modal Type Theory, Equational Theory, Soundness Proof, Linear Type Theory, Logical Framework, Contextual Modal Type Theory, Equational Theory, Soundness Proof",
author = "Anders Schack-Nielsen and Carsten Sch{\"u}rmann",
note = " TR-2011-151 ",
year = "2011",
language = "English",
isbn = "978-87-7949-250-9",
series = "IT University Technical Report Series",
number = "TR-2011-151",
publisher = "IT-Universitetet i K{\o}benhavn",
address = "Denmark",
edition = "TR-2011-151",
}