Stephanie Balzer
Skip Abstract Section
Abstract
Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous π-calculus into our language.
- Rob Arnold. 2010. C 0 , an Imperative Programming Language for Novice Computer Scientists. Master’s thesis. Department of Computer Science, Carnegie Mellon University. Available as Technical Report CMU-CS-10-145.Google Scholar
- Robert Atkey, Sam Lindley, and J. Garrett Morris. 2016. Conflation Confers Concurrency. In Wadler Festschrift, S. Lindley et al. (Ed.). Springer LNCS 9600, 32–55. Google ScholarCross Ref
- Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. Technical Report CMU-CS-17-106. Carnegie Mellon University.Google Scholar
- Romain Beauxis, Catuscia Palamidessi, and Frank D. Valencia. 2008. On the Asynchronous Nature of the Asynchronous π -calculus. In Concurrency, Graphs and Models (Lecture Notes in Computer Science), Vol. 5065. Springer, 473–492. Google ScholarDigital Library
- P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models. In 8th International Workshop on Computer Science Logic (CSL) (Lecture Notes in Computer Science), Vol. 933. Springer, 121–135. An extended version appeared as Technical Report UCAM-CL-TR-352, University of Cambridge.Google Scholar
- Kevin Bierhoff and Jonathan Aldrich. 2007. Modular Typestate Checking of Aliased Objects. In 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’07). ACM, 301–320. Google ScholarDigital Library
- John Boyland. 2003. Checking Interference with Fractional Permissions. In 10th International Symposium on Static Analysis (SAS). 55–72. Google ScholarCross Ref
- Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In 15th International Conference on Concurrency Theory (CONCUR) (Lecture Notes in Computer Science), Vol. 3170. Springer, 16–34. Google ScholarCross Ref
- Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In 21st International Conference on Concurrency Theory (CONCUR) (Lecture Notes in Computer Science), Vol. 6269. Springer, 222–236. Google ScholarCross Ref
- Luís Caires, Frank Pfenning, and Bernardo Toninho. 2016. Linear Logic Propositions as Session Types. Mathematical Structures in Computer Science 26, 3 (2016), 367–423. Google ScholarCross Ref
- Elias Castegren and Tobias Wrigstad. 2017. Relaxed Linear References for Lock-free Data Structures. In 31st European Conference on Object-Oriented Programming (ECOOP) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 74. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 6:1–6:32.Google Scholar
- Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins. 2002. A Concurrent Logical Framework II: Examples and Applications. Technical Report CMU-CS-02-102. Computer Science Department, Carnegie Mellon University. Revised May 2003.Google ScholarCross Ref
- Iliano Cervesato and Andre Scedrov. 2009. Relating State-Based and Process-Based Concurrency through Linear Logic. Information and Computation 207, 10 (2009), 1044–1077. Google ScholarDigital Library
- Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. 2003. A Judgmental Analysis of Linear Logic. Technical Report CMU-CS-03-131R. School of Computer Science, Carnegie Mellon University.Google Scholar
- Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a Recursive Module?. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 50–63. Google ScholarDigital Library
- Robert DeLine and Manuel Fähndrich. 2004. Typestates for Objects. In 18th European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science), Vol. 3086. Springer, 465–490. Google ScholarCross Ref
- Yuxin Deng, Robert J. Simmons, and Iliano Cervesato. 2016. Relating Reasoning Methodologies in Linear Logic and Process Algebra. Mathematical Structure in Computer Science 26, 5 (Jan. 2016), 868–906. Google ScholarCross Ref
- Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. 2012. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Proceedings of the 21st Conference on Computer Science Logic (CSL 2012), P. Cégielski and A. Durand (Eds.). Leibniz International Proceedings in Informatics, Fontainebleau, France, 228–242.Google Scholar
- Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. 2006. Session Types for Object-Oriented Languages. In 20th European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science), Vol. 4067. Springer, 328–352. Google ScholarDigital Library
- Edsger W. Dijkstra. 1971–1973. Hierarchical Ordering of Sequential Processes. (1971–1973). EWD Manuscript 310.Google Scholar
- Manuel Fähndrich and Robert DeLine. 2002. Adoption and Focus: Practical Linear Types for Imperative Programming. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 13–24. Google ScholarDigital Library
- Cormac Flanagan and Shaz Qadeer. 2003. A Type and Effect System for Atomicity. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 338–349. Google ScholarDigital Library
- Simon J. Gay and Malcolm Hole. 2005. Subtyping for Session Types in the π -Calculus. Acta Informatica 42, 2–3 (2005), 191–225.Google ScholarCross Ref
- David K. Gifford and John M. Lucassen. 1986. Integrating Functional and Imperative Programming. In LISP and Functional Programming. 28–38. Google ScholarDigital Library
- Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50 (1987), 1–102. Google ScholarDigital Library
- Dennis Griffith. 2016. Polarized Substructural Session Types. Ph.D. Dissertation. University of Illinois at Urbana-Champaign.Google Scholar
- Dennis Griffith and Frank Pfenning. 2015. SILL. https://github.com/ISANobody/sill . (2015).Google Scholar
- Robert Harper. 2013. Practical Foundations for Programming Languages. Cambridge University Press.Google Scholar
- Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers. 2013. Abstract Read Permissions: Fractional Permissions without the Fractions. In 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) (Lecture Notes in Computer Science), Vol. 7737. Springer, 315–334.Google Scholar
- Kohei Honda. 1993. Types for Dyadic Interaction. In 4th International Conference on Concurrency Theory (CONCUR) (Lecture Notes in Computer Science), Vol. 715. Springer, 509–523. Google ScholarCross Ref
- Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In 7th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science), Vol. 1381. Springer, 122–138. Google ScholarCross Ref
- Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty Asynchronous Session Types. In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 273–284. Google ScholarDigital Library
- W. A. Howard. 1969. The Formulae-as-Types Notion of Construction. (1969). Unpublished note. An annotated version appeared in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 479–490, Academic Press (1980).Google Scholar
- Raymond Hu, Nobuko Yoshida, and Kohei Honda. 2008. Session-Based Distributed Programming in Java. In 22nd European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science), Vol. 5142. Springer, 516–541. Google ScholarDigital Library
- Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015. Session Types for Rust. In 11th ACM SIGPLAN Workshop on Generic Programming (WGP).Google Scholar
- Limin Jia, Hannah Gommerstadt, and Frank Pfenning. 2016. Monitors and Blame Assignment for Higher-Order Session Types. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 582–594. Google ScholarDigital Library
- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 637–650. Google ScholarDigital Library
- Naoki Kobayashi and Cosimo Laneve. 2017. Deadlock Analysis of Unbounded Process Networks. Information and Computation 252 (2017), 48–70. Google ScholarDigital Library
- Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2017. Fencing off Go: Liveness and Safety for ChannelBased Programming. In 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 748–761. Google ScholarDigital Library
- K. Rustan M. Leino and Peter Müller. 2009. A Basis for Verifying Multi-Threaded Programs. In 18th European Symposium on Programming (ESOP). 378–393.Google Scholar
- Damiano Mazza. 2016. The True Concurrency of Differential Interaction Nets. Mathematical Structures in Computer Science (11 2016), 1–29. Google ScholarCross Ref
- Filipe Militão, Jonathan Aldrich, and Luís Caires. 2014. Rely-Guarantee Protocols. In 28th European Conference on ObjectOriented Programming (ECOOP) (Lecture Notes in Computer Science), Vol. 8586. Springer, 334–359. Google ScholarCross Ref
- Robin Milner. 1999. Communicating and Mobile Systems: the π -Calculus. Cambridge University Press.Google Scholar
- MozillaResearch. 2016. The Rust Programming Language. https://doc.rust- lang.org/stable/book . (November 2016).Google Scholar
- Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierhoff. 2012. A Type System for Borrowing Permissions. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 557–570. Google ScholarDigital Library
- Rumyana Neykova and Nobuko Yoshida. 2014. Multiparty Session Actors. In 16th International Conference on Coordination Models and Languages (COORDINATION) (Lecture Notes in Computer Science), Vol. 8459. Springer, 131–146. Google ScholarDigital Library
- Ligia Nistor, Jonathan Aldrich, Stephanie Balzer, and Hannes Mehnert. 2014. Object Propositions. In 19th International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science), Vol. 8442. Springer, 497–513. Google ScholarDigital Library
- Peter W. O’Hearn. 2004. Resources, Concurrency and Local Reasoning. In 15th International Conference on Concurrency Theory (CONCUR) (Lecture Notes in Computer Science), Vol. 3170. Springer, 49–67.Google Scholar
- Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. 2014. Linear Logical Relations and Observational Equivalences for Session-Based Concurrency. Information and Computation 239 (2014), 254–302. Google ScholarDigital Library
- Frank Pfenning. 2010. C0 Language. http://c0.typesafety.net. (2010).Google Scholar
- Frank Pfenning, Thomas J. Cortina, and William Lovas. 2011. Teaching Imperative Programming With Contracts at the Freshmen Level. (2011). Unpublished note.Google Scholar
- Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) (Lecture Notes in Computer Science), Vol. 9034. Springer, 3–22. Google ScholarCross Ref
- Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. (January 2009). http://www.cs.cmu.edu/~jcreed/papers/ jdml.pdf Unpublished manuscript.Google Scholar
- Davide Sangiorgi and David Walker. 2001. The π -Calculus - A Theory of Mobile Processes. Cambridge University Press.Google Scholar
- Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In 30th European Conference on Object-Oriented Programming (ECOOP) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 56. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 21:1–21:28.Google Scholar
- Jan Smans, Bart Jacobs, and Frank Piessens. 2009. Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. In 23rd European Conference on Object-Oriented Programming (ECOOP’09) (Lecture Notes in Computer Science), Vol. 5653. Springer, 148–172.Google Scholar
- Frederick Smith, David Walker, and J. Gregory Morrisett. 2000. Alias Types. In 9th European Symposium on Programming (ESOP). 366–381. Google ScholarCross Ref
- Robert E. Strom and Shaula Yemini. 1986. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering (TSE) 12, 1 (1986), 157–171. Google ScholarDigital Library
- Bernardo Toninho. 2015. A Logical Foundation for Session-based Concurrent Computation. Ph.D. Dissertation. Carnegie Mellon University and New University of Lisbon.Google Scholar
- Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: a Monadic Integration. In 22nd European Symposium on Programming (ESOP) (Lecture Notes in Computer Science), Vol. 7792. Springer, 350–369.Google ScholarDigital Library
- Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency. In 18th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, 377–390. Google ScholarDigital Library
- Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. Electronic Notes in Theoretical Computer Science 276 (2011), 335–351. Google ScholarDigital Library
- Philip Wadler. 1990. Linear Types Can Change the World!. In Woking Conference on Programming Concepts and Methods.Google Scholar
- Philip Wadler. 2012. Propositions as Sessions. In 17th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, 273–286. Google ScholarDigital Library
- David Walker and Kevin Watkins. 2001. On Regions and Linear Types. In 6th ACM SIGPLAN International Conference on Functional Programming (ICFP’06). ACM, 181–192.Google Scholar
- Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2002. A Concurrent Logical Framework I: Judgments and Properties. Technical Report CMU-CS-02-101. Computer Science Department, Carnegie Mellon University. Revised May 2003.Google ScholarCross Ref
- Max Willsey, Rokhini Prabhu, and Frank Pfenning. 2016. Design and Implementation of Concurrent C0. In Fourth International Workshop on Linearity.Google Scholar
Index Terms
- Manifest sharing with session types
Recommendations
Haskell session types with (almost) no class
HASKELL '08We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types ...
Gradual session types
Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type ...
Session types revisited
Session types are a formalism used to model structured communication-based programming. A binary session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session processes ...
Comments