Lincx: A Linear Logical Framework with First-class Contexts

Aina Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Abstract

Linear logic provides an elegant framework for modelling stateful, imperative and concurrent systems by viewing a context of assumptions as a set of resources. However, mechanizing the meta-theory of such systems remains a challenge, as we need to manage and reason about mixed contexts of linear and intuitionistic assumptions.

We present Lincx, a contextual linear logical framework with first-class mixed contexts. Lincx allows us to model (linear) abstract syntax trees as syntactic structures that may depend on intuitionistic and linear assumptions. It can also serve as a foundation for reasoning about such structures. Lincx extends the linear logical framework LLF with first-class (linear) contexts and an equational theory of context joins that can otherwise be very tedious and intricate to develop. This work may be also viewed as a generalization of contextual LF that supports both intuitionistic and linear variables, functions, and assumptions.

We describe a decidable type-theoretic foundation for Lincx that only characterizes canonical forms and show that our equational theory of context joins is associative and commutative. Finally, we outline how Lincx may serve as a practical foundation for mechanizing the meta-theory of stateful systems.
Original languageEnglish
Title of host publication26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings
PublisherSpringer
Publication date2017
Pages530-555
ISBN (Print)978-3-662-54433-4
ISBN (Electronic)978-3-662-54434-1
DOIs
Publication statusPublished - 2017
SeriesLecture Notes in Computer Science
Volume10201
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Lincx: A Linear Logical Framework with First-class Contexts'. Together they form a unique fingerprint.

Cite this