Document Open Access Logo

Type-Based Termination for Futures

Authors Siva Somayyajula , Frank Pfenning

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.12.pdf
  • Filesize: 0.83 MB
  • 21 pages

Document Identifiers

Author Details

Siva Somayyajula
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Frank Pfenning
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.
  • Somayyajula, Siva: Partially supported by the Sansom Graduate Fellowship in Computer Science.

Acknowledgements

We would like to thank Farzaneh Derakhshan, Klaas Pruiksma, Henry DeYoung, Ankush Das, and the anonymous reviewers for helpful discussion and suggestions regarding the contents of this paper.

Cite As Get BibTex

Siva Somayyajula and Frank Pfenning. Type-Based Termination for Futures. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.12

Abstract

In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our strong normalization result, which we develop via a novel logical relations argument.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Computing methodologies → Concurrent programming languages
Keywords
  • type-based termination
  • sized types
  • futures
  • concurrency
  • infinite proofs

Metrics

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

Related Versions

References

  1. Andreas Abel. Productive infinite objects via copatterns and sized types in agda. Google Scholar
  2. Andreas Abel. Semi-continuous Sized Types and Termination. Logical Methods in Computer Science, Volume 4, Issue 2, April 2008. Google Scholar
  3. Andreas Abel. Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In Dale Miller and Zoltán Ésik, editors, Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012, volume 77 of EPTCS, pages 1-11, 2012. URL: https://doi.org/10.4204/EPTCS.77.1.
  4. Andreas Abel and Brigitte Pientka. Well-founded recursion with copatterns and sized types. Journal of Functional Programming, 26:e2, 2016. Google Scholar
  5. Andrew W. Appel. Foundational proof-carrying code. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS '01, page 247, USA, 2001. IEEE Computer Society. Google Scholar
  6. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  7. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 42:1-42:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  8. Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto, and Tarmo Uustalu. Type-based termination of recursive definitions. Math. Struct. Comput. Sci., 14(1):97-141, 2004. URL: https://doi.org/10.1017/S0960129503004122.
  9. Henning Basold. Mixed inductive-coinductive reasoning: types, programs and logic. PhD thesis, Radboud University Nijmegen, April 2018. Google Scholar
  10. Frédéric Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, pages 24-39, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  11. Frédéric Blanqui and Colin Riba. Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In Miki Hermann and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 105-119, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  12. Frédéric Blanqui and Cody Roux. On the relation between sized-types based termination and semantic labelling. In 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Coimbra, Portugal, September 2009. Full version. Google Scholar
  13. James Brotherston. Cyclic Proofs for First-Order Logic with Inductive Definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 78-92, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  14. James Brotherston, Richard Bornat, and Cristiano Calcagno. Cyclic proofs of program termination in separation logic. In Proceedings of POPL-35, pages 101-112. ACM, 2008. Google Scholar
  15. Luís Caires and Frank Pfenning. Session Types as Intuitionistic Linear Propositions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222-236, Paris, France, August 2010. Springer LNCS 6269. Google Scholar
  16. Iliano Cervesato and Frank Pfenning. A linear logical framework. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS '96, page 264, USA, 1996. IEEE Computer Society. Google Scholar
  17. Iliano Cervesato and Andre Scedrov. Relating state-based and process-based concurrency through linear logic. Information and Computation, 207(10):1044-1077, 2009. Special issue: 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006). Google Scholar
  18. Jonathan Chan and William J. Bowman. Practical sized typing for coq. CoRR, abs/1912.05601, 2019. URL: http://arxiv.org/abs/1912.05601.
  19. Wei-Ngan Chin and Siau-Cheng Khoo. Calculating sized types. Higher-Order and Symbolic Computation, 14(2):261-300, 2001. Google Scholar
  20. Ioana Cristescu and Daniel Hirschkoff. Termination in a π-calculus with subtyping. Mathematical Structures in Computer Science, 26(8):1395-1432, 2016. Google Scholar
  21. Francesco Dagnino. Foundations of regular coinduction. Logical Methods in Computer Science, Volume 17, Issue 4, October 2021. URL: https://doi.org/10.46298/lmcs-17(4:2)2021.
  22. Nils Anders Danielsson and Thorsten Altenkirch. Mixing induction and coinduction, 2009. Google Scholar
  23. Ornela Dardha and Jorge A. Pérez. Comparing type systems for deadlock freedom. Journal of Logical and Algebraic Methods in Programming, 124:100717, 2022. Google Scholar
  24. Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. Subtyping on Nested Polymorphic Session Types, 2021. URL: http://arxiv.org/abs/2103.15193.
  25. Ankush Das and Frank Pfenning. Rast: A Language for Resource-Aware Session Types, 2020. URL: http://arxiv.org/abs/2012.13129.
  26. Ankush Das and Frank Pfenning. Session Types with Arithmetic Refinements. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  27. Ankush Das and Frank Pfenning. Verified Linear Session-Typed Concurrent Programming. In Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP '20, New York, NY, USA, 2020. Association for Computing Machinery. Google Scholar
  28. Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. Termination in impure concurrent languages. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 328-342, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  29. Yuxin Deng and Davide Sangiorgi. Ensuring termination by typability. Information and Computation, 204(7):1045-1082, 2006. Google Scholar
  30. Farzaneh Derakhshan and Frank Pfenning. Circular Proofs as Session-Typed Processes: A Local Validity Condition. CoRR, abs/1908.01909, August 2019. Google Scholar
  31. Farzaneh Derakhshan and Frank Pfenning. Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points. CoRR, abs/2001.05132, January 2020. Google Scholar
  32. Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 228-242, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  33. Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-Axiomatic Sequent Calculus. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1-29:22, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  34. Derek Dreyer, Amin Timany, Robbert Krebbers, Lars Birkedal, and Ralf Jung. What Type Soundness Theorem Do You Really Want to Prove?, October 2019. Google Scholar
  35. Elena Giachino, Naoki Kobayashi, and Cosimo Laneve. Deadlock analysis of unbounded process networks. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory, pages 63-77, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. Google Scholar
  36. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge University Press, USA, 1989. Google Scholar
  37. Robert H. Halstead. Multilisp: A language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst., 7(4):501-538, October 1985. Google Scholar
  38. Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson. Machine-checked semantic session typing. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 178-198, New York, NY, USA, 2021. Association for Computing Machinery. Google Scholar
  39. John Hughes, Lars Pareto, and Amr Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '96, pages 410-423, New York, NY, USA, 1996. Association for Computing Machinery. Google Scholar
  40. Aleksandar Ignjatovic. Hilbert’s program and the omega-rule, June 2018. Google Scholar
  41. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: Securing the foundations of the rust programming language. Proc. ACM Program. Lang., 2(POPL), December 2017. Google Scholar
  42. Naoki Kobayashi. A new type system for deadlock-free processes. In Christel Baier and Holger Hermanns, editors, CONCUR 2006 - Concurrency Theory, pages 233-247, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  43. Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. Integrating linear and dependent types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 17-30, New York, NY, USA, 2015. Association for Computing Machinery. Google Scholar
  44. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. SIGPLAN Not., 36(3):81-92, January 2001. Google Scholar
  45. Rodolphe Lepigre and Christophe Raffalli. Practical subtyping for Curry-style languages. ACM Trans. Program. Lang. Syst., 41(1), February 2019. Google Scholar
  46. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, USA, 2004. Google Scholar
  47. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. SIGPLAN Not., 51(9):434-447, September 2016. Google Scholar
  48. Hiroshi Nakano. A modality for recursion. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pages 255-266, 2000. Google Scholar
  49. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. Google Scholar
  50. Frank Pfenning. Types and Programming Languages, 2020. Google Scholar
  51. Klaas Pruiksma and Frank Pfenning. Back to Futures. CoRR, abs/2002.04607, February 2020. Google Scholar
  52. Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. Journal of Logical and Algebraic Methods in Programming, 120:100637, 2021. Google Scholar
  53. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254-302, 2014. Google Scholar
  54. Jorge Luis Sacchini. Linear Sized Types in the Calculus of Constructions. In Michael Codish and Eijiro Sumii, editors, Functional and Logic Programming, pages 169-185, Cham, 2014. Springer International Publishing. Google Scholar
  55. Davide Sangiorgi. Termination of processes. Mathematical Structures in Computer Science, 16(1):1-39, 2006. Google Scholar
  56. Paula Severi, Luca Padovani, Emilio Tuosto, and Mariangiola Dezani-Ciancaglini. On Sessions and Infinite Data. In Alberto Lluch Lafuente and José Proença, editors, Coordination Models and Languages, pages 245-261, Cham, 2016. Springer International Publishing. Google Scholar
  57. Siva Somayyajula. Towards Unifying (Co)induction and Structural Control. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Rome (virtual), Italy, June 2021. Google Scholar
  58. Gadi Tellez and James Brotherston. Automatically verifying temporal properties of pointer programs with cyclic proof. Journal of Automated Reasoning, 64(3):555-578, 2020. URL: https://doi.org/10.1007/s10817-019-09532-0.
  59. The Coq Development Team. The Coq Proof Assistant, January 2021. Google Scholar
  60. René Thiemann and Jürgen Giesl. Size-change termination for term rewriting. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications, pages 264-278, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. Google Scholar
  61. Bernardo Toninho, Luis Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems, pages 350-369, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  62. Andrea Vezzosi. Total (Co)Programming with Guarded Recursion. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), pages 77-78, Tallinn, Estonia, 2015. Institute of Cybernetics at Tallinn University of Technology. Google Scholar
  63. Philip Wadler. Propositions as sessions. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 273-286. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364568.
  64. Hongwei Xi. Dependent types for program termination verification. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pages 231-242, 2001. Google Scholar
  65. Hongwei Xi and Frank Pfenning. Dependent Types in Practical Programming. In A. Aiken, editor, Conference Record of the 26th Symposium on Principles of Programming Languages (POPL'99), pages 214-227. ACM Press, January 1999. Google Scholar
  66. Nobuko Yoshida. Graph types for monadic mobile processes. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, pages 371-386, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  67. Nobuko Yoshida, Martin Berger, and Kohei Honda. Strong normalisation in the π-calculus. Information and Computation, 191(2):145-202, 2004. 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