Biological systems encompass complexity that far surpasses many artificial systems. Modeling and simulation of large and complex biochemical pathways is a computationally intensive challenge. Traditional tools, such as ordinary differential equations, partial differential equations, stochastic master equations, and Gillespie type methods, are all limited either by their modeling fidelity or computational efficiency or both. In this work, we present a scalable computational framework based on modeling biochemical reactions in explicit 3D space, that is suitable for studying the behavior of large and complex biological pathways. The framework is designed to exploit parallelism and scalability offered by commodity massively parallel processors such as the graphics processing units (GPUs) and other parallel computing platforms. The reaction modeling in 3D space is aimed at enhancing the realism of the model compared to traditional modeling tools and framework. We introduce the Parallel Select algorithm that is key to breaking the sequential bottleneck limiting the performance of most other tools designed to study biochemical interactions. The algorithm is designed to be computationally tractable, handle hundreds of interacting chemical species and millions of independent agents by considering all-particle interactions within the system. We also present an implementation of the framework on the popular graphics processing units and apply it to the simulation study of JAK-STAT Signal Transduction Pathway. The computational framework will offer a deeper insight into various biological processes within the cell and help us observe key events as they unfold in space and time. This will advance the current state-of-the-art in simulation study of large scale biological systems and also enable the realistic simulation study of macro-biological cultures, where inter-cellular interactions are prevalent.

This special issue of Mathematical Structures in Computer Science is devoted to recent work in subtyping. When subtyping was first proposed, it presented a new vehicle for understanding programming languages, together with challenging theoretical issues. The papers in this special issue include a new approach to the decidability of subtyping, a metatheoretic investigation of transitivity of coercive subtyping for parametrised dependent types, and applications of subtyping to the classic programming language concerns of flow analysis and typing for distributed systems. We believe that the scope of the papers demonstrates convincingly that the theory and practice of subtyping continue to be extended in novel and interesting ways.

We defineBACI(Boxed Ambients with Communication Interfaces), an ambient calculus with a flexible communication policy. Traditionally, typed ambient calculi have a fixed communication policy determining the kind of information that can be exchanged with a parent ambient, even though mobility changes the parent.BACIlifts that restriction, allowing different communication policies with different parents during computation. Furthermore,BACIseparates communication and mobility by making the channels of communication between ambients explicit. In contrast with other typed ambient calculi where communication policies are global, each ambient inBACIis equipped with a description of the communication policies ruling its information exchange with parent and child ambients. The communication policies of ambients increase when they move: more precisely, when an ambient enters another ambient, the entering ambient and the host ambient can exchange their communication ports and agree on the kind of information to be exchanged. This information is recorded locally in both ambients. We show the type-soundness ofBACI, proving that it satisfies the subject reduction property, and we study its behavioural semantics by means of a labelled transition system.

We define BASS, a typed boxed ambients calculus with safe sessions. Sessions offer the possibility of using the same channel to transmit information of different types in a prescribed order. A session involves two communicating processes located either within the same ambient or across an ambient boundary. One of the challenges of adding session primitives to a mobile calculus is how to protect sessions from being interrupted by a mobility step. To address this challenge, we introduce a mechanism that prevents an ambient from moving, if there are pending sessions across its boundaryThe main result of our development is that in a well-typed process a communication redex never disappears after a mobility step. In other words, the residual of a communication redex is present in the reduct of the original process enabling a pending session step to be completed. Therefore, we claim that sessions in our calculus are safe.

This paper gives the first proof that the subtyping relation of a higher-order lambda calculus, -equality, which is apparently the first such, and shows its equivalence with the traditional presentation.

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al ., 1998). However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions (Clarke & Marrero, 1998; Gordon & Jeffrey, 2003b). The resulting type discipline augments the types of long-term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. This new type system can be used to check: source of information, whether data is propagated as specified across multiple parties, if there are unspecified communications between parties, and if the data being exchanged has been modified by the code in an unspecified way. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address shortcomings present in the pure theory of session types.

The need for subtyping in type-systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping extension of the system /spl lambda/P, which is an abstract version of the type system of the Edinburgh Logical Framework LF. By using an equivalent formulation, we establish some important properties of the new system /spl lambda/P/sub /spl les//, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking.

We study a natural generalization of SystemFωwith intersection types, establishing basic structural properties and constructing a semantic model based on partial equivalence relations to prove the soundness of typing. As an application of this calculus, we define a simple typed model of object-oriented programming with multiple inheritance.