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.
Original language | English |
---|
Publisher | IT-Universitetet i København |
---|---|
Number of pages | 6 |
ISBN (Print) | 978-87-7949-250-9 |
Publication status | Published - 2011 |
Bibliographical note
TR-2011-151
ID: 32757157