Typing with leftovers : a mechanization of Intuitionistic Multiplicative-Additive Linear Logic
Allais, Guillaume; Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus, eds. (2019) Typing with leftovers : a mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In: 23rd International Conference on Types for Proofs and Programs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, HUN, pp. 1-22. ISBN 1868-8969 (https://doi.org/10.4230/LIPIcs.TYPES.2017.1)
Preview |
Text.
Filename: Allais_TYPES2017_a_mechanization_of_Intuitionistic_Multiplicative_Additive_Linear_Logic.pdf
Final Published Version License: Download (629kB)| Preview |
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.
ORCID iDs
Allais, Guillaume ORCID: https://orcid.org/0000-0002-4091-657X; Abel, Andreas, Nordvall Forsberg, Fredrik and Kaposi, Ambrus-
-
Item type: Book Section ID code: 86659 Dates: DateEvent8 January 2019PublishedSubjects: Science > Mathematics > Electronic computers. Computer science > Other topics, A-Z Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 01 Sep 2023 14:04 Last modified: 28 Sep 2024 13:40 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/86659