Linear contextual modal type theory

Anders Schack-Nielsen, Carsten Schürmann

Publikation: Bog / Antologi / Rapport / Ph.D.-afhandlingRapportForskning

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.
OriginalsprogEngelsk
ForlagIT-Universitetet i København
Antal sider6
ISBN (Trykt)978-87-7949-250-9
StatusUdgivet - 2011

Citationsformater