License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2017.1
URN: urn:nbn:de:0030-drops-100490
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/10049/
Go to the corresponding LIPIcs Volume Portal

Allais, Guillaume

Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic

pdf-format:
LIPIcs-TYPES-2017-1.pdf (0.6 MB)

Abstract

We start from an untyped, well-scoped lambda-calculus and introduce a bidirectional typing relation corresponding to a Multiplicative-Additive Intuitionistic Linear Logic. We depart from typical presentations to adopt one that is well-suited to the intensional setting of Martin-Löf Type Theory. This relation is based on the idea that a linear term consumes some of the resources available in its context whilst leaving behind leftovers which can then be fed to another program.
Concretely, this means that typing derivations have both an input and an output context. This leads to a notion of weakening (the extra resources added to the input context come out unchanged in the output one), a rather direct proof of stability under substitution, an analogue of the frame rule of separation logic showing that the state of unused resources can be safely ignored, and a proof that typechecking is decidable. Finally, we demonstrate that this alternative formalization is sound and complete with respect to a more traditional representation of Intuitionistic Linear Logic.
The work has been fully formalised in Agda, commented source files are provided as additional material available at https://github.com/gallais/typing-with-leftovers.

BibTeX - Entry

@InProceedings{allais:LIPIcs:2018:10049,
  author =	{Guillaume Allais},
  title =	{{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and  Programs (TYPES 2017)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{104},
  editor =	{Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/10049},
  URN =		{urn:nbn:de:0030-drops-100490},
  doi =		{10.4230/LIPIcs.TYPES.2017.1},
  annote =	{Keywords: Type System, Bidirectional, Linear Logic, Agda}
}

Keywords: Type System, Bidirectional, Linear Logic, Agda
Collection: 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Issue Date: 2018
Date of publication: 08.01.2019
Supplementary Material: https://github.com/gallais/typing-with-leftovers

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI