Document Open Access Logo

Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description)

Authors Ankush Das , Frank Pfenning

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.33.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Ankush Das
  • Carnegie Mellon University, Pittsburgh, PA, USA
Frank Pfenning
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the National Science Foundation under Grant No. 1718276.

Acknowledgements

We would like to thank Farzaneh Derakhshan for contributions to the implementation and the anonymous reviewers for suggestions on an earlier version of this paper.

Cite AsGet BibTex

Ankush Das and Frank Pfenning. Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.33

Abstract

Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. Recent work has extended session types with refinements from linear arithmetic, capturing intrinsic properties of processes and data. These refinements then play a central role in describing sequential and parallel complexity bounds on session-typed programs. The Rast language and system provide an open-source implementation of session-typed concurrent programs extended with arithmetic refinements as well as ergometric and temporal types to capture work and span of program execution. Type checking relies on Cooper’s algorithm for quantifier elimination in Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast furthermore includes a reconstruction engine so that most program constructs pertaining the layers of refinements and resources are inserted automatically. We provide a variety of examples to demonstrate the expressivity of the language.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Linear logic
  • Theory of computation → Logic and verification
  • Computing methodologies → Concurrent programming languages
  • Theory of computation → Type theory
Keywords
  • Session Types
  • Resource Analysis
  • Refinement Types

Metrics

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

Supplementary Materials

References

  1. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proceedings of the 21st International Conference on Concurrency Theory, CONCUR'10, pages 222-236, Berlin, Heidelberg, 2010. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1887654.1887670.
  2. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 760, November 2014. URL: https://doi.org/10.1017/S0960129514000218.
  3. David C Cooper. Theorem proving in arithmetic without multiplication. Machine intelligence, 7(91-99):300, 1972. Google Scholar
  4. Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar. Resource-aware session types for digital contracts, 2019. URL: http://arxiv.org/abs/1902.06056.
  5. Ankush Das, Jan Hoffmann, and Frank Pfenning. Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang., 2(ICFP):91:1-91:30, July 2018. URL: https://doi.org/10.1145/3236786.
  6. Ankush Das, Jan Hoffmann, and Frank Pfenning. Work analysis with resource-aware session types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 305-314, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3209108.3209146.
  7. Ankush Das and Frank Pfenning. Session types with arithmetic refinements and their application to work analysis, 2020. URL: http://arxiv.org/abs/2001.04439.
  8. Farzaneh Derakhshan and Frank Pfenning. Circular Proofs as Session-Typed Processes: A Local Validity Condition. arXiv e-prints, page arXiv:1908.01909, August 2019. URL: http://arxiv.org/abs/1908.01909.
  9. Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut reduction in linear logic as asynchronous session-typed communication. In P. Cégielski and A. Durand, editors, Proceedings of the 21st Annual Conference on Computer Science Logic (CSL 2012), pages 228-242, Fontainebleau, France, September 2012. LIPIcs 16. Google Scholar
  10. Simon Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2):191-225, November 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  11. Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19-50, January 2010. Google Scholar
  12. Dennis Griffith and Elsa L. Gunter. Liquidpi: Inferrable dependent session types. In Guillaume Brat, Neha Rungta, and Arnaud Venet, editors, NASA Formal Methods, pages 185-197, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  13. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR'93, pages 509-523, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  14. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems, pages 122-138, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  15. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 273-284, New York, NY, USA, 2008. ACM. URL: https://doi.org/10.1145/1328438.1328472.
  16. Klaas Pruiksma and Frank Pfenning. A shared-memory semantics for mixed linear and non-linear session types. unpublished, 2018. Google Scholar
  17. Vasco T. Vasconcelos. Fundamentals of session types. Information and Computation, 217:52-70, 2012. URL: https://doi.org/10.1016/j.ic.2012.05.002.
  18. Philip Wadler. Propositions as sessions. SIGPLAN Not., 47(9):273–286, September 2012. URL: https://doi.org/10.1145/2398856.2364568.
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