Laws of Concurrent Programming

A simple but complete set of algebraic laws is given for a basic language (e.g., at the level of boogie). They include the algebraic properties of concurrency, similar to those of sequential composition. The laws are valid equally for interleaved concurrency and separated concurrency, and mixtures between them (e.g., as used in VCC). Most recognised methods of program analysis and verification are simply derived from the algebra. But will it be useful?

发言人详细信息

My first (and only) degree was from Oxford University in Classical Languages and Philosophy (1956). I learnt Russian in the Royal Navy (1958), Statistics at Oxford (1959), and spent a year at Moscow State University (1960). There I studied contemporary work on the machine translation of languages (English to Russian).

My first job was as a programmer for a small British Computer Manufacturer. I led the project which delivered the first commercial translator for ALGOL 60, before promotion to technical management in charge of development of all the Company’s software and hardware products. I then spent two years in the Research Laboratory, before the Company was merged into a much larger one.

This was the cue to move (1968) as Professor, to the Queen’s University, Belfast, where I pursued longer-term research into the role of assertions as a scientific basis for the design of programs and of programming languages. The research continued and intensified on my move to Oxford University in 1977. My laboratory established a good record for collaboration with Industry in both hardware and software design; we won several awards, and spun off several Companies that still flourish.

On reaching retirement age for an academic in Britain, I gladly took up an offer to return to Industry at Microsoft Research in Cambridge. My goal remains the same: to build good links between academic research into programming theory, and industrial practices contributing to timely delivery of high quality software.

日期：
演讲者：
Tony Hoare
所属机构：
MSR Cambridge