Abstract We present a programming language for describing and analysing concurrent quantum systems. We have an interpreter for programs in the language, using a symbolic rather than a numeric calculator, and we give its performance on examples from quantum communication and cryptography.

Abstract Simpson and Harris have described multi-slot algorithms implementing a single-place buffer, each operating without explicit hardware synchronisation mechanisms. Conventional refinement and proof techniques have explained that these algorithms work, but do not give convincing descriptions of how they work. An unconventional refinement process starting from the classic single-variable buffer, using both data and atomicity refinement and drawing information from unsuccessful steps, derives each algorithm. The logic used is RGSep, a marriage of rely/guarantee and concurrent separation logic. Extensive detailed verifications are described. The result is an explanation of how the algorithms work and some pointers to how such algorithms might be devised.

Abstract Separation logic allows simple proofs of concurrent algorithms which use blocking mechanisms such as semaphores. It can even deal with non-blocking algorithms. With the addition of mechanisms borrowed from rely-guarantee, we can make reasonably simple proofs of some simple non-blocking algorithms. We show that it extends to proofs of some intricate algorithms, including Simpson’s famous asynchronous four-slot buffer and Harris’s novel three-slot algorithm, in a manner that is arguably simpler than earlier treatments, though we cannot claim that we have yet found proofs that are as simple as we would wish. Our example proofs show functional correctness but do not deal with questions of liveness.

Peter Landin, who has died recently of prostate cancer, was an outstanding academic computer scientist who set the direction of the subject for his generation.In an astonishing burst of creativity in the 1950s and 1960s he showed that programs could be defined in terms of mathematical functions, how to translate them into functional expressions in the lambda calculus, the creation of Alonso Church in 1936, and how to calculate their meaning with an abstract mathematical machine, prefiguring many of the advances of the next couple of decades.Although later he turned away from computer science towards gay politics, he remained an original and extreme thinker, a complex and intriguing character.An only child born in Sheffield, son of an accountant father disabled in WW1, he was educated at King Edward's Grammar School.During National Service he amused himself by trying to drill a squad to imitate addition in binary arithmetic.At Clare College Cambridge he completed the mathematics degree in two years, then attempted the very difficult part 3, but came away with only a 3rd class degree.The emerging computing industry was a haven for mavericks, though, and he took a job at English Electric, where he cooperated in the development of EE's Deuce from the National Physical Laboratory's early Pilot Ace.His ideas had already turned to the problems of relating the mathematics of logic to the ad-hoc languages invented by programmers.He was involved in the discussions which led to the development of Algol 60, a seminal programming language of the time, though he failed to convince the committee that it should be defined in terms of substitution as in the lambda calculus.His interests drew him into Mervyn Pragnell's discussion group.Mervyn used to prowl bookshops spotting people who were buying books on mathematical logic and invite them to his group which read and discussed the books in a kind of perpetual cycle.Despite the depth of his understanding compared to the rest of the group, Peter was always kind and helpful to novices and stragglers, and even programmers could join and learn.In 1960 he married Hanne and he was taken on as a research assistant by Christopher Strachey, then an independent consultant and later Professor at Oxford, to write a compiler to translate 'autocode', an early programming language, into the machine language of Ferranti's new Orion machine.He envisaged the compiler as an automatic product of the semantics of the autocode, matching its forms to semantic representations of the instructions of the machine, and generating LISP expressions that could be executed, but his attempt was never finished, and it was a long time before such a radical approach became feasible.He was held in awe by the elite

We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system.Judgements in this system express (guaranteed) termination of the program when started from a given line in the program and in a state satisfying a given precondition, which is expressed as a formula of separation logic. The proof rules of our system are of two types: logical rules that operate on preconditions; and symbolic execution rules that capture the effect of executing program commands.

This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which is essential to the algorithm, is confined in the proof and the specification to the modular operations, which perform push and pop on the stack. This is achieved by the mechanisms of separation logic. The effect is that inter-thread interference does not pollute specification or verification of clients of the stack.

Hoare logic is bedevilled by complex but coarse side conditions on the use of variables. We define a logic, free of side conditions, which permits more precise statements of a program’s use of variables. We show that it admits translations of proofs in Hoare logic, thereby showing that nothing is lost, and also that it admits proofs of some programs outside the scope of Hoare logic. We include a treatment of reference parameters and global variables in procedure call (though not of parameter aliasing). Our work draws on ideas from separation logic: program variables are treated as resource rather than as logical variables in disguise. For clarity we exclude a treatment of the heap.

A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads, subdivision and combination of permission is discussed. The roots of the approach are in Boyland's [3] demonstration of the utility of fractional permissions in specifying non-interference between concurrent threads. We add the notion of counting permission, which mirrors the programming technique called permission counting. Both fractional and counting permissions permit passivity, the specification that a program can be permitted to access a heap cell yet prevented from altering it. Models of both mechanisms are described. The use of two different mechanisms is defended. Some interesting problems are acknowledged and some intriguing possibilities for future development, including the notion of resourcing as a step beyond typing, are paraded.

Jape is a program which supports the step-by-step interactive development of proofs in formal logics, in the style of proofs-on-paper. It is uncommitted to any particular logic and is customized by a description of a collection of inference rules and the syntax of judgements. It works purely at the surface syntactic level, as a person working on paper might. In that spirit it makes use of explicit visible provisos rather than a conventional encoding of logical properties. Its principal mechanism is unification, employed as a search tool to defer decisions about how to proceed at difficult points in a proof. The design aim is to produce a tool which makes step-by-step proof calculations so straightforward that novices can learn by exploring the use of a pre-encoded logic. Examples of proof development are given in several small logics.

Abstract. GUI design isn't simply a matter of putting a nice front-end on a capable program. It requires thought about the way in which people might be expected to use a system, and investigation of the ways that they actually use it. Jape's GUI has been designed to be as simple as possible, so that it will not get in the way of the business of proof. It is designed to be minimal in the information that it displays and the gestures that it requires from the user. In this paper we introduce and give a rationale for the design of Jape's user interface, then note some of its drawbacks.

There has been an explosion of interest in the use of logic in computer science in recent years. This is in part due to theoretical developments within academic computer science and in part due to the recent popularity of Formal Methods amongst software engineers. There is now a widespread and growing popularity of Formal Methods amongst software engineers. There is now a widespread and growing recognition that formal techniques are central to the subject and that a good grasp of them is essential for a practising computer scientist. This recognition that computer science has become a much more rigorous subject has lead a number of influential academics to call for changes to its curriculum that reflect this new rigour [8,12]. At the same time, it is a commonplace amongst computer science teachers that students find formal techniques difficult to learn. The growth of interest in logic has therefore been accompanied by a further recognition that certain kinds of mechanical support are necessary in order for logic to be used effectively. The purpose of this article is to describe a number of programs which have been developed to support the teaching of logic. Three broad criteria have been used in evaluating these systems. We consider their logical generality (the power of the encoded logic), their usability (the quality of the user interface) and their pedagogic value as teaching tools. We hope the review will act as a useful reference for the design and development of logic curricular within computer science.