Document Open Access Logo

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

Author Guillaume Allais

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2017.1.pdf
  • Filesize: 0.59 MB
  • 22 pages

Document Identifiers

Author Details

Guillaume Allais
  • iCIS, Radboud University Nijmegen, The Netherlands

Funding

The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement nr. 320571

Cite As Get BibTex

Guillaume Allais. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.TYPES.2017.1

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Linear logic
Keywords
  • Type System
  • Bidirectional
  • Linear Logic
  • Agda

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Peter Achten, John Van Groningen, and Rinus Plasmeijer. High level specification of I/O in functional languages. In Functional Programming, Glasgow 1992, pages 1-17. Springer, 1993. Google Scholar
  2. Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning, 2015. URL: http://arxiv.org/abs/1511.09230.
  3. Guillaume Allais and Conor McBride. Certified Proof Search for Intuitionistic Linear Logic, 2015. URL: http://gallais.github.io/proof-search-ILLWiL/.
  4. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, pages 182-199. Springer, 1995. Google Scholar
  5. Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic, pages 453-468. Springer, 1999. Google Scholar
  6. Robert Atkey and James Wood. Sorting Types - Permutation via Linearity. https://github.com/bobatkey/sorting-types, 2013. Retrieved on 2017-11-06.
  7. Andrew Barber and Gordon Plotkin. Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science, 1996. Google Scholar
  8. Nick Benton, Gavin Bierman, Valeria De Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. Typed Lambda Calculi and Applications, pages 75-90, 1993. Google Scholar
  9. Richard S. Bird and Ross Paterson. de Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77–91, 1999. Google Scholar
  10. Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Theoretical Aspects of Computer Software, pages 515-529. Springer, 1997. Google Scholar
  11. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23(05):552-593, 2013. Google Scholar
  12. Edwin Brady, Conor McBride, and James McKinna. Inductive families need not store their indices. In Types for proofs and programs, pages 115-129. Springer, 2003. Google Scholar
  13. Edwin Brady and Matúš Tejišcák. Practical Erasure in Dependently Typed Languages. Google Scholar
  14. Iliano Cervesato, Joshua S Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In International Workshop on Extensions of Logic Programming, pages 67-81. Springer, 1996. Google Scholar
  15. James Maitland Chapman. Type checking and normalisation. PhD thesis, University of Nottingham, 2009. Google Scholar
  16. Pierre-Evariste Dagand and Conor McBride. Transporting functions across ornaments. Journal of Functional Programming, 24(2-3):316-383, 2014. Google Scholar
  17. Nils Danielsson. Bag Equivalence via a Proof-Relevant Membership Relation. Interactive Theorem Proving, pages 149-165, 2012. Google Scholar
  18. Olivier Danvy. Type-Directed Partial Evaluation. In Partial Evaluation, pages 367-411. Springer, 1999. Google Scholar
  19. Nicolaas Govert De Bruijn. Lambda Calculus Notation with Nameless Dummies. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. Elsevier, 1972. Google Scholar
  20. The Rust Project Developers. The Rust Programming Language - Ownership. https://doc.rust-lang.org/book/first-edition/ownership.html, 2017. Retrieved on 2017-11-06.
  21. Peter Dybjer. Inductive families. Formal aspects of computing, 6(4):440-465, 1994. Google Scholar
  22. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  23. Oleg Kiselyov. Typed tagless final interpreters. In Generic and Indexed Programming, pages 130-174. Springer, 2012. Google Scholar
  24. Robbert Krebbers. The C standard formalized in Coq. PhD thesis, Radboud University Nijmegen, 2015. Google Scholar
  25. John Launchbury and Simon L Peyton Jones. Lazy functional state threads. In ACM SIGPLAN Notices, volume 29, pages 24-35. ACM, 1994. Google Scholar
  26. Olivier Laurent and Laurent Regnier. Linear Logic Wiki - Intuitionistic Linear Logic. http://llwiki.ens-lyon.fr/mediawiki/index.php/Intuitionistic_linear_logic, 2009. Retrieved on 2017-11-06.
  27. Pierre Letouzey. A new extraction for Coq. In Types for proofs and programs, pages 200-219. Springer, 2002. Google Scholar
  28. Conor McBride. Ornamental algebras, algebraic ornaments. Journal of functional programming, 2010. Google Scholar
  29. Conor McBride. I Got Plenty o’Nuttin’. In A List of Successes That Can Change the World, pages 207-233. Springer, 2016. Google Scholar
  30. John C Mitchell. Foundations for programming languages, volume 1. MIT press, 1996. Google Scholar
  31. Ulf Norell. Dependently typed programming in Agda. In Advanced Functional Programming, pages 230-266. Springer, 2009. Google Scholar
  32. Benjamin C Pierce and David N Turner. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1):1-44, 2000. Google Scholar
  33. Jeff Polakow. Embedding a full linear lambda calculus in Haskell. ACM SIGPLAN Notices, 50(12):177-188, 2016. Google Scholar
  34. Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In Quantum Physics and Logic, 2017. Google Scholar
  35. Anne Sjerp Troelstra. Lectures on linear logic. Center for the Study of Language and Inf, 1991. Google Scholar
  36. Stephanie Weirich, Justin Hsu, and Richard A Eisenberg. Towards dependently typed Haskell: System FC with kind equality. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. Citeseer, 2013. Google Scholar
  37. Michael Winiko and James Harland. Deterministic resource management for the linear logic programming language Lygon. Technical report, Technical Report 94/23, Melbourne University, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact