TY - RPRT

T1 - Linear contextual modal type theory

AU - Schack-Nielsen, Anders

AU - Schürmann, Carsten

N1 - TR-2011-151

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

M3 - Report

SN - 978-87-7949-250-9

BT - Linear contextual modal type theory

PB - IT-Universitetet i København

ER -