Linear contextual modal type theory

Anders Schack-Nielsen, Carsten Schürmann

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

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

Keywords

  • Linear Type Theory
  • Logical Framework
  • Contextual Modal Type Theory
  • Equational Theory
  • Soundness Proof

Fingerprint

Dive into the research topics of 'Linear contextual modal type theory'. Together they form a unique fingerprint.

Cite this