Publications
373 results found
Scalas A, Dardha O, Hu R, et al., 2017, A linear decomposition of multiparty sessions for safe distributed programming, Departmental Technical Report: 17/2, Publisher: Department of Computing, Imperial College London, 17/2
Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processesthat can ensure properties such as absence of communication errors and deadlocks, andprotocol conformance. Can MPST provide a theoretical foundation for concurrent and distributedprogramming in “mainstream” languages?We address this problem by (1) developing the first encoding of a full-fledged multipartysession -calculus into standard linear -calculus, and (2) using the encoding as the foundationof a practical toolchain for safe multiparty programming in Scala.Our encoding is type-preserving and operationally sound and complete. Importantly fordistributed applications, it preserves the choreographic nature of MPST and illuminates thatmultiparty sessions (and their safety properties) can be precisely represented with a decompositioninto binary linear channels. Previous works have only studied the relation between (limited)multiparty sessions and binary sessions by orchestration means.We exploit these results to implement an automated generation of Scala APIs for multipartysessions. These APIs act as a layer on top of existing libraries for binary communication channels:this allows distributed multiparty systems to be safely implemented over binary transports, ascommonly found in practice. Our implementation is also the first to support distributed multipartydelegation: our encoding yields it for free, via existing mechanisms for binary delegation.
Scalas A, Yoshida N, 2017, Multiparty session types, beyond duality, Departmental Technical Report: 17/4, 17/4
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processesinteracting on sessions involving two or more participants. Session typing can ensure desirableproperties: absence of communication errors and deadlocks, and protocol conformance. However,existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly)restrictive: it only holds for typing contexts with strong duality constraints on the interactionsbetween pairs of participants. Consequently, many “intuitively correct” examples cannot be typedand/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason forthese limitations. Then, we present a novel MPST typing system that removes these restrictions.
Neykova R, Yoshida N, 2017, How to Verify Your Python Conversations, BEHAVIOURAL TYPES: FROM THEORY TO TOOLS, Editors: Gay, Ravara, Publisher: RIVER PUBLISHERS, Pages: 77-98, ISBN: 978-87-93519-82-4
Kouzapas D, Perez JA, Yoshida N, 2016, Characteristic bisimulation for higher-order session processes, Acta Informatica, Vol: 54, Pages: 271-341, ISSN: 1432-0525
For higher-order (process) languages, characterising contextual equivalence is a long-standing issue. In the setting of a higher-order \(\pi \)-calculus with session types, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.
Toninho B, Yoshida N, 2016, Certifying data in multiparty session types, Journal of Logical and Algebraic Methods in Programming, Vol: 90, Pages: 61-83, ISSN: 2352-2208
Multiparty session types (MPST) are a typing discipline for ensuring the coordination of multi-agent communication in concurrent and distributed programs. The original MPST framework mainly focuses on the communication aspects of concurrency, unable to capture important data invariants in communicating programs. This work introduces value dependent types to the MPST framework in order to increase its expressiveness for certifying invariants of data exchanged among multiple participants. The key idea is to impose constraints on the exchanged data, which is explicitly witnessed at runtime by proof objects. The enriched MPST framework provides programmers with a precise global description of the interaction and data dependent patterns, from which local (data dependent) descriptions can be automatically generated for each endpoint, faithfully capturing at a local level the global data constraints. The framework ensures the absence of communication errors and guarantees communication progress in well-typed multiparty sessions. We also develop an extension of value dependencies based on proof irrelevance that enables the selective erasure of proof objects at runtime.
Carbone M, Montesi F, Schürmann C, et al., 2016, Multiparty session types as coherence proofs, Acta Informatica, Vol: 54, Pages: 243-269, ISSN: 0001-5903
We propose a Curry–Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.
Niu X, Ng C, Yumi T, et al., 2016, EURECA compilation: Automatic optimisation of cycle-reconfigurable circuits, 26th International Conference on Field-Programmable Logic and Applications, Publisher: IEEE
EURECA architectures have been proposed as anenhancement to the existing FPGAs, to enable cycle-by-cyclereconfiguration. Applications with irregular data accesses, whichpreviously cannot be efficiently supported in hardware, canbe efficiently mapped into EURECA architectures. One majorchallenge to apply the EURECA architectures to practicalapplications is the intensive design efforts required to analyseand optimise cycle-reconfigurable operations, in order to obtainaccurate and high-performance results while underlying circuitsreconfigure cycle by cycle. In this work, we propose compilersupport for EURECA-based designs. The compiler supportadopts techniques based on session types to automatically derive aruntime reconfiguration scheduler that guarantees design correct-ness; and a streaming circuit model to ensure high-performancecircuits. Three benchmark applications —large-scale sorting,Memcached, and SpMV— developed with the proposed compilersupport show up to 11.2 times (21.8 times when architecturescales) reduction in area-delay product when compared withconventional architectures, and achieve up to39%improvementscompared with manually optimised EURECA designs.
Zhou H, Niu X, Yuan J, et al., 2016, Connect on the fly: enhancing and prototyping of cycle-reconfigurable modules, 26th International Conference on Field-Programmable Logic and Applications, Publisher: IEEE
This paper introduces cycle-reconfigurable modulesthat enhance FPGA architectures with efficient support fordynamic data accesses: data accesses with accessed data size andlocation known only at runtime. The proposed module adoptsnew reconfiguration strategies based ondynamic FIFOs,dynamiccaches, anddynamic shared memoriesto significantly reduceconfiguration generation and routing complexity. We developa prototype FPGA chip with the proposed cycle-reconfigurablemodule in the SMIC 130-nm technology. The integrated moduletakes less than the chip area of 39 CLBs, and reconfiguresthousands of runtime connections in 1.2 ns. Applications for large-scale sorting, sparse matrix-vector multiplication, and Mem-cached are developed. The proposed modules enable 1.4 and11 times reductions in area-delay product compared with thoseapplications mapped to previous architectures and conventionalFPGAs.
Clemente TM, Cortez C, Novaes ADS, et al., 2016, Surface Molecules Released by <i>Trypanosoma cruzi</i> Metacyclic Forms Downregulate Host Cell Invasion, PLOS NEGLECTED TROPICAL DISEASES, Vol: 10, ISSN: 1935-2735
- Author Web Link
- Cite
- Citations: 12
Ancona D, Bono V, Bravetti M, et al., 2016, Behavioral types in programming languages, Foundations and Trends in Programming Languages, Vol: 3, Pages: 95-230, ISSN: 2325-1107
A recent trend in programming language research is to use behav-ioral type theory to ensure various correctness properties of large-scale, communication-intensive systems. Behavioral types encompassconcepts such as interfaces, communication protocols, contracts, andchoreography. The successful application of behavioral types requiresa solid understanding of several practical aspects, from their represen-tation in a concrete programming language, to their integration withother programming constructs such as methods and functions, to de-sign and monitoring methodologies that take behaviors into account.This survey provides an overview of the state of the art of these aspects,which we summarize as thepragmaticsof behavioral types.
Scalas A, Yoshida N, 2016, Lightweight Session Programming in Scala, 30th European Conference on Object-Oriented Programming (ECOOP 2016), Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Pages: 21:1-21:28, ISSN: 1868-8969
Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.
Tiezzi F, Yoshida N, 2016, Reversing Single Sessions, 8th International Conference on Reversible Computation (RC 2016), Publisher: Springer International Publishing, Pages: 52-69, ISSN: 0302-9743
Session-based communication has gained a widespread acceptance in practice as a means for developing safe communicating systems via structured interactions. In this paper, we investigate how these structured interactions are affected by reversibility, which provides a computational model allowing executed interactions to be undone. In particular, we provide a systematic study of the integration of different notions of reversibility in both binary and multiparty single sessions. The considered forms of reversibility are: one for completely reversing a given session with one backward step, and another for also restoring any intermediate state of the session with either one backward step or multiple ones. We analyse the costs of reversing a session in all these different settings. Our results show that extending binary single sessions to multiparty ones does not affect the reversibility machinery and its costs.
Cortez C, Real F, Yoshida N, 2016, Lysosome biogenesis/scattering increases host cell susceptibility to invasion by <i>Trypanosoma cruzi</i> metacyclic forms and resistance to tissue culture trypomastigotes, CELLULAR MICROBIOLOGY, Vol: 18, Pages: 748-760, ISSN: 1462-5814
- Author Web Link
- Cite
- Citations: 35
Ferreira ER, Horjales E, Bonfim-Melo A, et al., 2016, Unique behavior of <i>Trypanosoma cruzi</i> mevalonate kinase: A conserved glycosomal enzyme involved in host cell invasion and signaling, SCIENTIFIC REPORTS, Vol: 6, ISSN: 2045-2322
- Author Web Link
- Cite
- Citations: 21
Parente Coutinho Fernandes Toninho B, Yoshida N, 2016, Certifying Data in Multiparty Session Types, WadlerFest, Publisher: Springer, Pages: 433-458, ISSN: 0302-9743
Multiparty session types (MPST) are a typing discipline for ensuringthe coordination and orchestration of multi-agent communication in concurrentand distributed programs. However, by mostly focusing on the communication aspectsof concurrency, MPST are often unable to capture important data invariantsin programs. In this work we propose to increase the expressiveness of MPSTby considering a notion of value dependencies in order to certify invariants ofexchanged data in concurrent and distributed settings.
Lange J, Yoshida N, 2016, Characteristic Formulae for Session Types, TACAS 2016, Publisher: Springer, Pages: 833-850, ISSN: 0302-9743
Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem. Our core contribution is an algorithm to generate a modal μμ-calculus formula that characterises all the supertypes (or subtypes) of a given type. Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely. We have implemented our theory and compared its cost with other classical subtyping algorithms.
Perera R, Lange J, Gay S, 2016, Multiparty compatibility for concurrent objects, International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, Publisher: Open Publishing Association, Pages: 73-82, ISSN: 2075-2180
Objects and actors are communicating state machines, offering and consuming different services atdifferent points in their lifecycle. Two complementary challenges arise when programming suchsystems. When objects interact, their state machines must be “compatible”, so that services arerequested only when they are available. Dually, when objects refine other objects, their state machinesmust be “compliant”, so that services are honoured whenever they are promised.In this paper we show how the idea of multiparty compatibility from the session types literaturecan be applied to both of these problems. We present an untyped language in which concurrent objectsare checked automatically for compatibility and compliance. For simple objects, checking can beexhaustive and has the feel of a type system. More complex objects can be partially validated via testcases, leading to a methodology closer to continuous testing. Our proof-of-concept implementationis limited in some important respects, but demonstrates the potential value of the approach and therelationship to existing software development practices.
Orchard D, Yoshida N, 2016, Electronic Proceedings in Theoretical Computer Science, EPTCS: Preface, PLACES 2016, ISSN: 2075-2180
Orchard D, Yoshida N, 2016, Effects as sessions, sessions as effects, ACM SIGPLAN Notices, Vol: 51, Pages: 568-581, ISSN: 0362-1340
Maeda FY, Clemente TM, Macedo S, et al., 2016, Host cell invasion and oral infection by <i>Trypanosoma cruzi</i> strains of genetic groups TcI and TcIV from chagasic patients, PARASITES & VECTORS, Vol: 9, ISSN: 1756-3305
- Author Web Link
- Cite
- Citations: 16
Honda K, Yoshida N, Carbone M, 2016, Multiparty asynchronous session types, Journal of the ACM, Vol: 63, ISSN: 0004-5411
Communication is becoming one of the central elements in software development. As a potential typed foundationfor structured communication-centred programming, session types have been studied over the lastdecade for a wide range of process calculi and programming languages, focussing on binary (two-party)sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions,which often arise in practical communication-centred applications. Presented as a typed calculus formobile processes, the theory introduces a new notion of types in which interactions involving multiple peersare directly abstracted as a global scenario. Global types retain the friendly type syntax of binary sessiontypes while specifying dependencies and capturing complex causal chains of multiparty asynchronous interactions.A global type plays the role of a shared agreement among communication peers, and is used as abasis of efficient type checking through its projection onto individual peers. The fundamental properties ofthe session type discipline such as communication safety, progress and session fidelity are established forgeneral n-party asynchronous interactions.
Kouzapas D, Perez J, Yoshida N, 2016, On the Relative Expressiveness of Higher-Order Session Processes, ESOP 2016, Publisher: Springer, Pages: 446-475, ISSN: 0302-9743
By integrating constructs from the λλ-calculus and the ππ-calculus, in higher-order process calculi exchanged values may contain processes. This paper studies the relative expressiveness of HOπHOπ, the higher-order ππ-calculus in which communications are governed by session types. Our main discovery is that HOHO, a subcalculus of HOπHOπ which lacks name-passing and recursion, can serve as a new core calculus for session-typed higher-order concurrency. By exploring a new bisimulation for HOHO, we show that HOHO can encode HOπHOπ fully abstractly (up to typed contextual equivalence) more precisely and efficiently than the first-order session ππ-calculus (ππ). Overall, under session types, HOπHOπ, HOHO, and ππ are equally expressive; however, HOπHOπ and HOHO are more tightly related than HOπHOπ and ππ.
Hu R, Yoshida N, 2016, Hybrid Session Verification through Endpoint API Generation, FASE 2016, Publisher: Springer, Pages: 401-418, ISSN: 0302-9743
This paper proposes a new hybrid session verification methodology for applying session types directly to mainstream languages, based on generating protocol-specific endpoint APIs from multiparty session types. The API generation promotes static type checking of the behavioural aspect of the source protocol by mapping the state space of an endpoint in the protocol to a family of channel types in the target language. This is supplemented by very light run-time checks in the generated API that enforce a linear usage discipline on instances of the channel types. The resulting hybrid verification guarantees the absence of protocol violation errors during the execution of the session. We implement our methodology for Java as an extension to the Scribble framework, and use it to specify and implement compliant clients and servers for real-world protocols such as HTTP and SMTP.
Ng N, Yoshida N, 2016, Static deadlock detection for concurrent go by global session graph synthesis, 25th International Conference on Compiler Construction (CC 2016), Publisher: ACM, Pages: 174-184
Go is a programming language developed at Google, with channel-based concurrent features based on CSP. Go can detect global communication deadlocks at runtime when all threads of execution are blocked, but deadlocks in other paths of execution could be undetected. We present a new static analyser for concurrent Go code to find potential communication errors such as communication mismatch and deadlocks at compile time. Our tool extracts the communication operations as session types, which are then converted into Communicating Finite State Machines (CFSMs). Finally, we apply a recent theoretical result on choreography synthesis to generate a global graph representing the overall communication pattern of a concurrent program. If the synthesis is successful, then the program is free from communication errors. We have implemented the technique in a tool, and applied it to analyse common Go concurrency patterns and an open source application with over 700 lines of code.
Dezani-Ciancaglini M, Ghilezan S, Jakšić S, et al., 2016, Denotational and operational preciseness of subtyping: A roadmap, Lecture Notes in Computer Science, Publisher: Springer, Pages: 155-172, ISBN: 9783319307336
The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in object-oriented programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type, which is a mathematical object describing the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The present paper shows that standard proofs of operational preciseness imply denotational preciseness and gives an overview on this subject.
Debois S, Hildebrandt T, Slaats T, et al., 2016, Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion, Logical Methods in Computer Science, Vol: 12, Pages: 1-38, ISSN: 1860-5974
We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.
Debois S, Hildebrandt T, Slaats T, et al., 2016, Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion, Logical Methods in Computer Science, Vol: 12, ISSN: 1860-5974
We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.
Dezani-Ciancaglini M, Ghilezan S, Jakšić S, et al., 2016, Precise subtyping for synchronous multiparty sessions, Electronic Proceedings in Theoretical Computer Science, Vol: 203, Pages: 29-43, ISSN: 2075-2180
The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.
Orchard D, Yoshida N, 2016, Using session types as an effect system, Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2015), Publisher: "Electronic Proceedings in Theoretical Computer Science, ISSN: 2075-2180
Side effects are a core part of practical programming. However, they are often hard to reason about, particularly in a concurrent setting. We propose a foundation for reasoning about concurrent side effects using sessions. Primarily, we show that session types are expressive enough to encode an effect system for stateful processes. This is formalised via an effect-preserving encoding of a simple imperative language with an effect system into the pi-calculus with session primitives and session types (into which we encode effect specifications). This result goes towards showing a connection between the expressivity of session types and effect systems. We briefly discuss how the encoding could be extended and applied to reason about and control concurrent side effects.
Orchard D, Yoshida N, 2016, Effects as sessions, sessions as effects, 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), Publisher: ACM, Pages: 568-581
Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the lambda-calculus and its variants, the latter for the pi-calculus. In this paper we explore their relative expressive power. Firstly, we give an embedding from PCF, augmented with a parameterised effect system, into a session-typed pi-calculus (session calculus), showing that session types are powerful enough to express effects. Secondly, we give a reverse embedding, from the session calculus back into PCF, by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result. We also discuss various extensions to our embeddings.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.