@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",

author = "Anders Schack-Nielsen and Carsten Sch{\"u}rmann",

note = " TR-2011-151 ",

year = "2011",

language = "English",

isbn = "978-87-7949-250-9",

publisher = "IT-Universitetet i K{\o}benhavn",

address = "Denmark",

}