A talk about quantum computing and quantum cryptography, with focus on formal analysis, and a little light simulation.
Watch the video
View the presentations
- Qtpi: Simulating (Concurrent) Quantum Systems (PDF)
Richard Bornat - Formal Modelling, Programming & Verification of Quantum Systems (PDF)
Rajagopal Nagarajan
Synopsis
The novel fields of quantum computation and quantum information have gathered significant impetus in the last few years, and it has the potential to radically impact the future of information technology and society. The successful construction of a large-scale fault-tolerant quantum computer may be some years away.
However, many applications are being developed now to run on near-term NISQ (Noisy Intermediate Scale Quantum) computers which are easily accessible over the internet. Secure communication using quantum cryptography has also been implemented. The major selling point of quantum cryptography is unconditional security.
But can this be guaranteed in practice?
Even when protocols have been mathematically proved to be secure, it is notoriously difficult to achieve robust and reliable implementations of secure systems. Formal verification is widely used by industry to ensure that (classical) systems meet their specifications.
In this talk, we will give an overview of some of our ongoing work in using techniques from typed programming languages, model- and equivalence-checking, theorem proving, and testing to the modelling and analysis of quantum systems. There will be a short demonstration of some simulations of simple quantum protocols.
About the speakers
Rajagopal Nagarajan is Professor of Foundations of Computing at Middlesex University London.
He leads a group of academics working in various areas of theoretical computer science and its applications. Prior to that he was Associate Professor at the University of Warwick, UK. Nagarajan received his PhD from Imperial College London and has held research positions at ATC-NY, USA, the University of Calgary, Canada and the University of California, Berkeley, USA. His research interests are in Quantum Computing and Cryptography, Foundations of Programming Languages, Formal Methods, Information Security, Machine Learning and Financial Computing.
Richard Bornat is Emeritus Professor of Computer Programming at Middlesex University.
He has a background in compiling, programming language design, and separation logic. He is co-author of the logic calculator Jape. He has held academic positions at Essex University, Queen Mary College London, and Middlesex University. His research interests are dwindling but remain centred in logic and programming.
Our events are for adults aged 16 years and over.
For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.
This event is brought to you by: BCS FACS (Formal Aspects of Computing Science) group
