Linear contextual modal type theory

Anders Schack-Nielsen, Carsten Schürmann

Research output: Book / Anthology / Report / Ph.D. thesisReportResearch


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.
Original languageEnglish
PublisherIT-Universitetet i København
Number of pages6
ISBN (Print)978-87-7949-250-9
Publication statusPublished - 2011

Cite this