Dynamically typed languages are very well suited for rapid prototyping, agile programming methodologies and rapidly evolving software. However, programmers can still benefit from the ability to detect type errors in their code early, in particular if this does not impose restrictions on their programming style. In this paper we describe a new type checking system that identifies potential type errors in such languages through a flow-sensitive static analysis. It computes for every expression the variable's present (from the values that it has last been assigned) and future (with which it is used in the further program execution) types, respectively. Using this information, the mechanism inserts type checks at strategic points in the original program. We prove that these checks are inserted as early as possible and preempt type errors earlier than existing type systems. We further show that these checks do not change the semantics of programs that do not raise type errors. Preemptive type checking can be added to existing languages without the need to modify the existing runtime environment. Instead, it can be invoked at a very late stage, after the compilation to bytecode and initialisation of the program. We demonstrate an implementation of this for the Python language, and its effectiveness on a number of standard benchmarks. (C) 2018 Elsevier Inc. All rights reserved.

We introduce a divide-and-conquer algorithm for a modified version of the reachability/coverability problem in 1-bounded Petri nets that relies on the compositional algebra of nets with boundaries: we consider the algebraic decomposition of the net of interest as part of the input. We formally prove the correctness of the technique and contrast the performance of our implementation with state-of-the-art tools that exploit partial order reduction techniques on the global net.

We describe a type system that identifies potential type errors in dynamically typed languages like Python. The system uses a flow-sensitive static analysis on bytecodes to compute, for every variable and program point, over-approximations of the variable’s present and future use types. If the future use types are not subsumed by the present types, the further program execution may raise a type error, and a narrowing assertion is inserted; if future use and present types are disjoint, it will raise a type error, and a type error assertion is inserted. We prove that the assertions are inserted in optimal locations and thus preempt type errors earlier than dynamic, soft, and gradual typing. We describe the details of our type inference and assertion insertion, and demonstrate the results of an implementation of the system with a number of examples.

In recent work, the second and third authors introduced a technique for reachability checking in 1-bounded Petri nets, based on wiring decompositions, which are expressions in a fragment of the compositional algebra of nets with boundaries. Here we extend the technique to the full algebra and introduce the related structural property of decomposition width on directed hypergraphs. Small decomposition width is necessary for the applicability of the reachability checking algorithm. We give examples of families of nets with constant decomposition width and develop the underlying theory of decompositions.

Global Session Types are typically used to express communication protocols between a number of participating entities. Analyses on these types can be used to prove that message passing programs have a variety of desirable properties such as communications safety and deadlock freedom. In this paper we provide a Global Session Type analysis for queued channel message passing programs whose code may be updated during runtime (Dynamic Software Update). In particular, we prove safety and liveness properties for well-typed programs by identifying suitable restrictions on the runtime points at which dynamic updates may occur. This includes the possibility of updating several threads without requiring global thread synchronisation.

We investigate and implement a model of typed streaming I/O. Each type determines a language of traces analogous to regular expressions on strings, and programs are modelled by certain monotone functions on these traces. We show that sequential composition forms a lax braided monoid in the category of types and programs. This lax braided structure allows programs to be represented diagrammatically using Joyal and Street's string diagrams in 3D space. Monotone functions over traces cannot be executed efficiently, so we present an equivalent monoidal category of transducers. We demonstrate that transducers can be executed efficiently, theoretically by showing that programs with diagrams embedded in the plane can be executed in O(1) space, and experimentally by an implementation in the Agda dependently typed functional language. Agda supports machine-assisted proof: we have mechanically verified that the transducer implementation and the I/O model form lax braided monoidal categories.

Randomization is used in computer security as a tool to introduce unpredictability into the software infrastructure. In this paper, we study the use of randomization to achieve the secrecy and integrity guarantees for local memory. We follow the approach set out by Abadi and Plot kin. We consider the execution of an idealized language in two environments. In the strict environment, opponents cannot access local variables of the user program. In the lax environment, opponents may attempt to guess allocated memory locations and thus, with small probability, gain access the local memory of the user program. We model these environments using two novel calculi: lambda-mu-hashref and lambda-mu-proberef. Our contribution to the Abadi-Plot kin program is to enrich the programming language with dynamic memory allocation, first class and higher order references and call/cc-style control. On the one hand, these enhancements allow us to directly model a larger class of system hardening principles. On the other hand, the class of opponents is also enhanced since our enriched language permits natural and direct encoding of attacks that alter the control flow of programs. Our main technical result is a fully abstract translation (up to probability) of lambda-mu-hashref into lambda-mu-proberef. Thus, in the presence of randomized layouts, the opponent gains no new power from being able to guess local references of the user program. Our numerical bounds are similar to those of Abadi and Plot kin, thus, the extra programming language features do not cause a concomitant increase in the resources required for protection via randomization.

Manually implementing equals (for object comparisons) and hashCode (for object hashing) methods in large software projects is tedious and error-prone. This is due to many special cases, such as field shadowing, comparison between different types, or cyclic object graphs. Here, we present JEqualityGen, a source code generator that automatically derives implementations of these methods. JEqualityGen proceeds in two states: it first uses source code reflection in MetaAspectJ to generate aspects that contain the method implementations, before it uses weaving on the bytecode level to insert these into the target application. JEqualityGen generates not only correct, but efficient source code that on a typical large-scale Java application exhibits a performance improvement of more than two orders of magnitude in the equality operations generated, compared to an existing system based on runtime reflection. JEqualityGen achieves this by generating runtime profiling code that collects data. This enables it to generate optimised method implementations in a second round.

We develop local reasoning techniques for message passing concurrent programs based on ideas from separation logics and resource usage analysis. We extend processes with permission- resources and define a reduction semantics for this extended language. This provides a foundation for interpreting separation formulas for message-passing concurrency. We also define a sound proof system permitting us to infer satisfaction compositionally using local, separation-based reasoning.

Manually implementing equals (for object comparisons) and hashCode (for object hashing) methods in large software projects is tedious and error-prone. This is due to many special cases, such as field shadowing, comparison between different types, or cyclic object graphs. Here, we present JEqualityGen, a source code generator that automatically derives implementations of these methods. JEqualityGen proceeds in two states: it first uses source code reflection in MetaAspectJ to generate aspects that contain the method implementations, before it uses weaving on the bytecode level to insert these into the target application. JEqualityGen generates not only correct, but efficient source code that on a typical large-scale Java application exhibits a performance improvement of more than two orders of magnitude in the equality operations generated, compared to an existing system based on runtime reflection. JEqualityGen achieves this by generating runtime profiling code that collects data. This enables it to generate optimised method implementations in a second round.

Determining equality of objects in Java requires the implementation of equals and hashCode methods. Such an implementation has to follow a specic object contract, making it a very tedious and error-prone process. Many equality and hashing methods implemented in Java applications violate this contract and are faulty, due to complexity arising from eld shadowing, comparisons between dierent types, object cycles, etc. Equality and hashing implementations are conceptually simple, and can be derived automatically from information obtained statically from the program. However, existing systems that generate equality implementations use reection and are consequently inecient. Here we describe JEqualityGen, a source code generator that seamlessly integrates with the build process of typical Java projects: the programmer only needs to indicate for which classes implementations should be generated. JEqualityGen produces correct and ecient code which on a typical large-scale Java application exhibits a typical performance improvement of 162 in the equality operations generated by existing reective systems. This was made possible through the use of optimised code generation and runtime proling of these methods.

Behavioural equivalences of various calculi for modelling distributed systems differ significantly because the properties which can be observed through interaction depend heavily upon their mode of communication. A typical approach to describing the semantics of communicating processes is to provide a labelled transition system (LTS) which captures the interaction potential of the individual processes within a larger system. In many cases, a natural rendering of this LTS leads to too fine a semantics as unobservability of certain communications is not accounted for.We propose that a standard approach to augmenting LTSs allows morally unobservable communications to actually be modelled as unobservables in the semantics. This approach derives from a rule initially given by Honda and Tokoro to account for unobservability of reception in the asynchronous pi-calculus. We examine the implications of adding such rules to LTS with respect to the proving behavioural equivalences for various

Dynamic software update is a technique by which a running program can be updated with new code and data without interrupting its execution. Often we will want to preserve properties of programs across update boundaries. Preserving simple typing across update boundaries for single-threaded programs is well studied. There are other higher-level properties we may wish to preserve, particularly for multi-threaded programs. Session typing is used to guarantee that a set of parallel threads communicate according to a given protocol. Hence we investigate preserving correct communications behaviour of a set of parallel threads correctly across update boundaries which change the running protocol. We present a procedure for updating multiple threads to cleanly migrate a system from one protocol to another.

We re-examine the standard structural operational semantics of the π-calculus with the view that both process structure and contextual observational power should play roles in describing the behavioural theory. To that end we provide a decomposition of the operational semantics of π which allows for a systematic definition of labelled transitions. These are derived from the calculus' underlying reduction rules by following the contexts-as-labels philosophy while being presented using the structural approach. Our novel transition system refines to a composite description of the standard early lts. We generalise our technique to higher-order and asynchronous variants.

We present a new labelled transition system (lts) for the ambient calculus on which ordinary bisimilarity coincides with contextual equivalence. The key feature of this ltsis that it is the fruit of ongoing work on developing a systematic procedure for deriving ltss in the structural style from the underlying reduction semantics and observability. Notably, even though we have derived our ltsfor ambients systematically it compares very favourably with existing transition systems for the same calculus.

We use the framework of biorthogonality to introduce a novel semantic definition of the concept of barb (basic observable) for process calculi. We develop a uniform basic theory of barbs and demonstrate its robustness by showing that it gives rise to the correct observables in specific process calculi which model synchronous, asynchronous and broadcast communication regimes.

We introduce a novel technique for the development of coinductive characterisations of contextually-defined equivalence for the Picalculus. The technique relies on splitting the derivation rules for labelled transition systems (LTSs) into two separate modular subsystems: a process-view and a context-view of interactions. In order to do so we introduce a typed meta-syntax for representing terms with holes. The approach yields a new context bisimulation for first-order Pi which refines to a composite description of the standard early LTS. The technique generalises to higher-order and asynchronous variants to give a modular account of their features.

We present a type and effect system for statically determin- ing whether concurrent programs in a simple functional language adhere to a strict access control policy. Policy states are represented by automata states and are tracked, statically, by the type and effect system. We en- sure that, per thread, all function calls are, independently, in accordance with policy with respect to the current state. To verify that several con- current threads jointly satisfy a policy we are required to explore the state space of an interleaving of the several threads' effects. However, we observe that by furnishing our language with monitor synchronisation primitives we can reduce our state space search by abstracting away be- haviours inside atomic sections. The type and effect system is proved to satisfy Subject Reduction and a Safety theorem which guarantees that well-typed programs never violate policy.