Document Open Access Logo

Encoding Tight Typing in a Unified Framework

Authors Delia Kesner , Andrés Viso

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.27.pdf
  • Filesize: 0.87 MB
  • 20 pages

Document Identifiers

Author Details

Delia Kesner
  • Université de Paris, CNRS, IRIF, France
  • Institut Universitaire de France (IUF), France
Andrés Viso
  • Inria, Paris, France

Funding

This work has been partially supported by IRP SINFIN.

Acknowledgements

We are specially grateful to G. Guerrieri for fruitful discussions. We also thank B. Accattoli, A. Bucciarelli, and A. Ríos for constructive remarks.

Cite AsGet BibTex

Delia Kesner and Andrés Viso. Encoding Tight Typing in a Unified Framework. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 27:1-27:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.27

Abstract

This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, i.e. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Call-by-Push-Value
  • Call-by-Name
  • Call-by-Value
  • Intersection Types

Metrics

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

Related Versions

References

  1. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1-94:30, 2018. URL: https://doi.org/10.1145/3236789.
  2. Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 206-226, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_12.
  3. Beniamino Accattoli and Giulio Guerrieri. Types of fireballs. In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 45-66. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_3.
  4. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 410-439. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_15.
  5. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, 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.
  6. Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, volume 7294 of Lecture Notes in Computer Science, pages 4-16. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29822-6_4.
  7. Sandra Alves, Delia Kesner, and Daniel Ventura. A quantitative understanding of pattern matching. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway, volume 175 of LIPIcs, pages 3:1-3:36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.3.
  8. Hendrik P. Barendregt. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland, revised edition, 1984. Google Scholar
  9. Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:3)2013.
  10. Marc Bezem, Jan Willem Klop, and Vincent van Oostrom. Term Rewriting Systems (TeReSe). Cambridge University Press, 2003. Google Scholar
  11. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Logic, 109(3):205-241, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
  12. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. In Keisuke Nakano and Konstantinos Sagonas, editors, Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings, volume 12073 of Lecture Notes in Computer Science, pages 13-32. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_2.
  13. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Solvability = typability + inhabitation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7141.
  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. Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  16. Jules Chouquet and Christine Tasson. Taylor expansion for call-by-push-value. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 16:1-16:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.16.
  17. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  18. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. Sequent calculi for second order logic. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic. Cambridge University Press, 1995. Google Scholar
  19. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université Aix-Marseille II, 2007. Google Scholar
  20. Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 41:1-41:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.41.
  21. 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.
  22. Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Inf. Comput., 248:104-129, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.010.
  23. Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A semantic measure of the execution time in linear logic. Theor. Comput. Sci., 412(20):1884-1902, 2011. URL: https://doi.org/10.1016/j.tcs.2010.12.017.
  24. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 259-273. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.259.
  25. Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 202-228. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_9.
  26. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 174-187. ACM, 2016. URL: https://doi.org/10.1145/2967973.2968608.
  27. Claudia Faggian and Giulio Guerrieri. Factorization in call-by-name and call-by-value calculi via linear logic. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12650 of Lecture Notes in Computer Science, pages 205-225. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_11.
  28. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  29. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  30. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  31. Giulio Guerrieri. Towards a semantic measure of the execution time in call-by-value lambda-calculus. In Michele Pagani and Sandra Alves, editors, Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems, DCM/ITRS 2018, Oxford, UK, 8th July 2018, volume 293 of EPTCS, pages 57-72, 2018. URL: https://doi.org/10.4204/EPTCS.293.5.
  32. Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two girard’s translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA), Oxford, UK, 7-8 July 2018., EPTCS, pages 15-30, 2019. Google Scholar
  33. Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing connected proof(-structure)s from their taylor expansion. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.20.
  34. Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-by-value, again! In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 7:1-7:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.7.
  35. Delia Kesner and Pierre Vial. Types as resources for classical natural deduction. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 24:1-24:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.24.
  36. Delia Kesner and Pierre Vial. Consuming and persistent types for classical logic. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 619-632. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394774.
  37. Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. CoRR, abs/2105.00564, 2021. URL: http://arxiv.org/abs/2105.00564.
  38. Zurab Khasidashvili. The Church-Rosser theorem in orthogonal combinatory reduction systems. Technical Report 1825, INRIA Rocquencourt, France, 1992. Google Scholar
  39. Jan Willem Klop. Combinatory reduction systems. PhD thesis, Univ. Utrecht, 1980. Google Scholar
  40. Maico Leberle. Dissecting call-by-need by customizing multi type systems. PhD thesis, Institut Polytechnique de Paris, 2021. Google Scholar
  41. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Google Scholar
  42. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377-414, 2006. URL: https://doi.org/10.1007/s10990-006-0480-6.
  43. Giulio Manzonetto, Michele Pagani, and Simona Ronchi Della Rocca. New semantical insights into call-by-value λ-calculus. Fundam. Informaticae, 170(1-3):241-265, 2019. URL: https://doi.org/10.3233/FI-2019-1862.
  44. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. Proc. ACM Program. Lang., 2(POPL):6:1-6:28, 2018. URL: https://doi.org/10.1145/3158094.
  45. Laurent Regnier. Une équivalence sur les lambda-termes. TCS, 2(126):281-292, 1994. Google Scholar
  46. José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal embeddings and calling paradigms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., volume 131 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.18.
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 Imprint Privacy Contact