Computer Science research project receives Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award

Dr Arnold Beckmann (Computer Science, Swansea University), in collaboration with Dr Norbert Preining (Japan Advanced Institute of Science and Technology), has been awarded a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award over £12000. The project entitled “Hypersequents and Communication” runs from January 2014 for two years, and involves several mutual visits.

A celebrated result, bridging proof theory and theory of computation, is given by the Curry-Howard correspondence.  It enables us to see proofs of formulas expressing specifications as programs solving the specification.  Furthermore, due to the Curry-Howard correspondence, such programs can be formally verified to satisfy their specification, a property of growing importance in our times of ubiquitous computing, in particular in safety critical areas.  The Curry-Howard correspondence also had an enormous impact on the development of formal proof assistant tools like Coq, and functional programming languages like CAML.

Furthermore, it has been the origin of Linear Logic, one of the main tools for understanding the operational content of proofs.

The aim of this project is to go beyond the traditional Curry-Howard correspondence and extended it to a wider class of proof theoretic calculi, and a wider class of computational models.  In particular, we want to treat communication and parallelism in a similar way.

The project started with a kick-off "Workshop on Proofs as Processes" in Kanasawa, Ishikawa, Japan, 20-21 January 2014, see http://www.jaist.ac.jp/~preining/wpp/.