Linear contextual modal type theory
Research output: Book / Anthology / Report / Ph.D. thesis › Report › Research
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.
|Publisher||IT-Universitetet i København|
|Number of pages||6|
|Publication status||Published - 2011|