Abstract We build on a fine-grained analysis of session-based interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. A remarkable feature of the SAM’s design is its ability to naturally segregate and coordinate sequential with concurrent session behaviours. In particular, implicitly sequential parts of session programs may be efficiently executed by deterministic sequential application of SAM transitions, amenable to compilation, and without concurrent synchronisation mechanisms. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its correctness for executing programs in a session calculus corresponding to full classical linear logic $$\textsf{CLL}$$ CLL . We also discuss extensions and applications of the SAM to the execution of linear and session-based programming languages.

Abstract We introduce $$\textsf{CLASS}$$ CLASS , a session-typed, higher-order, core language that supports concurrent computation with shared linear state.

invited-talk Share on A Decade of Dependent Session Types Authors: Bernardo Toninho NOVA School of Science and Technology and NOVA-LINCS, Portugal NOVA School of Science and Technology and NOVA-LINCS, PortugalView Profile , Luís Caires NOVA School of Science and Technology and NOVA-LINCS, Portugal NOVA School of Science and Technology and NOVA-LINCS, PortugalView Profile , Frank Pfenning Carnegie Mellon University, USA Carnegie Mellon University, USAView Profile Authors Info & Claims PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative ProgrammingSeptember 2021 Article No.: 3Pages 1–3https://doi.org/10.1145/3479394.3479398Online:07 October 2021Publication History 0citation24DownloadsMetricsTotal Citations0Total Downloads24Last 12 Months24Last 6 weeks8 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

We develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.

We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation. Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting.

This work introduces the novel concept of kind refinement , which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles expressed by predicates over values in the type domain, kind refinements provide rich kind specifications by means of predicates over types in the kind domain. By leveraging our powerful refinement kind discipline, types in our language are not just used to statically classify program expressions and values, but also conveniently manipulated as tree-like data structures, with their kinds refined by logical constraints on such structures. Remarkably, the resulting typing and kinding disciplines allow for powerful forms of type reflection, ad-hoc polymorphism and type-directed meta-programming, which are often found in modern software development, but not typically expressible in a type-safe manner in general purpose languages. We validate our approach both formally and pragmatically by establishing the standard meta-theoretical results of type safety and via a prototype implementation of a kind checker, type checker and interpreter for our language.

The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

Throughout the years, several typing disciplines for the π-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input/output behaviour of processes and traditionally provide strong guarantees about this behaviour (i.e. deadlock-freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood. This paper proposes a type system for the π-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut-elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems.

In this paper, we develop a novel notion of dependent information flow types. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values.

We introduce the concept of behavioral separation as a general principle for disciplining interference in higher-order imperative concurrent programs, and present a type-based approach that systematically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives. Behavioral separation builds on notions originally introduced for behavioral type systems and separation logics, but shifts the focus from the separation of static program state properties towards the separation of dynamic usage behaviors of runtime values. Behavioral separation types specify how values may be safely used by client code, and can enforce fine-grained interference control disciplines while preserving compositionality, information hiding, and flexibility. We illustrate how our type system, even if based on a small set of general primitives, is already able to tackle fairly challenging program idioms, involving aliasing at various types, concurrency with first-class threads, manipulation of linked data structures, behavioral borrowing, and invariant-based separation.

We develop an interpretation of linear type theory as dependent session types for a term passing extension of the pi-calculus. The type system allows us to express rich constraints on sessions, such as interface contracts and proof-carrying certification, which go beyond existing session type systems, and are here justified on purely logical grounds. We can further refine our interpretation using proof irrelevance to eliminate communication overhead for proofs between trusted parties. Our technical results include type preservation and global progress, which in our setting naturally imply compliance to all properties declared in interface contracts expressed by dependent types.

Tracking the state of an object (in the sense of how a File can be in an Open or Closed state) is difficult not just because of the problem of managing state transitions but also due to the complexity introduced by aliasing. Unchecked duplication of object references makes local reasoning impossible by allowing situations where transitions can be triggered unexpectedly (for instance, passing aliased parameters to a method that expects unaliased parameters, or calling a method that has a side effect through an alias deeply nested in a data structure).