Document Open Access Logo

A Deep Quantitative Type System

Authors Giulio Guerrieri , Willem B. Heijltjes, Joseph W.N. Paulus

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.24.pdf
  • Filesize: 0.62 MB
  • 24 pages

Document Identifiers

Author Details

Giulio Guerrieri
  • University of Bath, Department of Computer Science, UK
Willem B. Heijltjes
  • University of Bath, Department of Computer Science, UK
Joseph W.N. Paulus
  • Rijksuniversiteit Groningen, The Netherlands

Funding

This work was supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing.

Acknowledgements

We would like to thank Ugo Dal Lago, Delia Kesner, Luc Pelissier, Nicolas Wu, and the anonymous referees for their constructive engagement with our work.

Cite As Get BibTex

Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus. A Deep Quantitative Type System. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.24

Abstract

We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the "collection calculus", as a Curry-Howard interpretation of the type system, that embodies these computational properties.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Lambda calculus
Keywords
  • Lambda-calculus
  • Deep inference
  • Intersection types
  • Resource calculus

Metrics

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

References

  1. Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In 23rd International Conference on Rewriting Techniques and Applications, RTA 2012, volume 15 of LIPIcs, pages 6-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.6.
  2. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, 30:e14, 2020. URL: https://doi.org/10.1017/S095679682000012X.
  3. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference, volume 6247 of Lecture Notes in Computer Science, pages 381-395. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_30.
  4. Beniamino Accattoli and Delia Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:28)2012.
  5. Juan P. Aguilera and Matthias Baaz. Unsound inferences make proofs shorter. Journal of Symbolic Logic, 84(1):102-122, 2019. URL: https://doi.org/10.1017/jsl.2018.51.
  6. Andrea Aler Tubella and Alessio Guglielmi. Subatomic proof systems: Splittable systems. ACM Transactions on Computational Logic (TOCL), 19(1):5:1-5:33, 2018. URL: https://doi.org/10.1145/3173544.
  7. Hendrik Pieter Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  8. Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. In International Conference on Typed Lambda Calculi and Applications, TLCA '93, volume 664 of Lecture Notes in Computer Science, pages 75-90. Springer, 1993. URL: https://doi.org/10.1007/BFb0037099.
  9. Gérard Boudol. The lambda-calculus with multiplicities. In CONCUR '93, 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 1-6. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_1.
  10. Kai Brünnler and Richard McKinley. An algorithmic interpretation of a deep inference system. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, volume 5330 of Lecture Notes in Computer Science, pages 482-496. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_34.
  11. Kai Brünnler and Alwen Tiu. A local system for classical logic. In Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, volume 2250 of Lecture Notes in Computer Science, pages 347-361. Springer, 2001. URL: https://doi.org/10.1007/3-540-45653-8_24.
  12. Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, and Michel Parigot. Quasipolynomial normalisation in deep inference via atomic flows. Logical Methods in Computer Science, 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:5)2016.
  13. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, 109(3):205-241, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
  14. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/jigpal/jzx018.
  15. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for lambda-terms. Archiv für mathematische Logik und Grundlagenforschung, 19(1):139-156, 1978. URL: https://doi.org/10.1007/BF02011875.
  16. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  17. Ugo Dal Lago, Giulio Guerrieri, and Willem Heijltjes. Decomposing probabilistic lambda-calculi. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, volume 12077 of Lecture Notes in Computer Science, pages 136-156. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_8.
  18. Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, volume 62 of LIPIcs, pages 41:1-41:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.41.
  19. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  20. Thomas Ehrhard. Non-idempotent intersection types in logical form. In Foundations of Software Science and Computation Structures, FoSSaCS 2020, volume 12077 of Lecture Notes in Computer Science, pages 198-216. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_11.
  21. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  22. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403:347-372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  23. Philippa Gardner. Discovering needed reductions using type theory. In Theoretical Aspects of Computer Software, International Conference TACS '94, volume 789 of Lecture Notes in Computer Science, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  24. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, 1998. URL: https://doi.org/10.1006/inco.1998.2700.
  25. Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A proof calculus which reduces syntactic bureaucracy. In 21st International Conference on Rewriting Techniques and Applications, RTA 2010, volume 6 of LIPIcs, pages 135-150. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.RTA.2010.135.
  26. Tom Gundersen, Willem Heijltjes, and Michel Parigot. Atomic lambda-calculus: a typed lambda-calculus with explicit sharing. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 311-320. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.37.
  27. Willem Heijltjes and Joe Paulus. Deep-inference intersection types. Extended abstract, presented at the workshop Twenty Years of Deep Inference (TYDI), Oxford, 2018. Available at http://willem.heijltj.es/pdf/2018-heijltjes-paulus.pdf, 2018.
  28. Emil Jeřábek. Proof complexity of the cut-free calculus of structures. Journal of Logic and Computation, 19(2):323-339, 2009. URL: https://doi.org/10.1093/logcom/exn054.
  29. Delia Kesner and Stéphane Lengrand. Resource operators for lambda-calculus. Information and Computation, 205(4):419-473, 2007. URL: https://doi.org/10.1016/j.ic.2006.08.008.
  30. Assaf J. Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411-436, 2000. URL: https://doi.org/10.1093/logcom/10.3.411.
  31. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 301-310. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  32. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. Proceedings of the ACM on Programming Languages, 2(POPL), 2018. URL: https://doi.org/10.1145/3158094.
  33. C.-H. Luke Ong. Quantitative semantics of the lambda-calculus: Some generalisations of the relational model. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005064.
  34. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science, 27(5):626-650, 2017. URL: https://doi.org/10.1017/S0960129515000316.
  35. Elaine Pimentel, Simona Ronchi Della Rocca, and Luca Roversi. Intersection Types from a proof-theoretic perspective. Fundamenta Informaticae, 121(1-4):253-274, 2012. URL: https://doi.org/10.3233/FI-2012-778.
  36. Garrel Pottinger. A type assignment for the strongly normalizable lambda-terms. In J. Hindley and J. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561-577. Academic Press, 1980. Google Scholar
  37. David Sherratt, Willem Heijltjes, Tom Gundersen, and Michel Parigot. Spinal atomic lambda-calculus. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, volume 12077 of Lecture Notes in Computer Science, pages 582-601. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_30.
  38. Alwen Tiu. A local system for intuitionistic logic. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, volume 4246 of Lecture Notes in Computer Science, pages 242-256. Springer, 2006. URL: https://doi.org/10.1007/11916277_17.
  39. Alwen Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2):4:1-24, 2006. URL: https://doi.org/10.2168/LMCS-2(2:4)2006.
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