|
Actual Introductory Talks |
|
Page 8 of 8
Introduction to logics as type theories for quantum processes
|
Samson Abramsky, Oxford University, UK
|
|
Introductory lecture summary:
Traditional quantum logic studies *properties* of quantum processes. Another logical paradigm has become important in Computer Science over the past 3 decades. Here one views formulas as *types*, and *proofs as (typed) programs* or processes. This paradigm is ripe for application to quantum computation. In particular, `resource sensitive' logics such as Linear logic seem appropriate, because their restrictions on `structural rules of inference' correspond to fundamental informatic restrictions imposed by Quantum Mechanics: specifically, No Cloning and No Deleting. Such logics arise as the logics of tensor or monoidal categories, which have been used by the present author and Bob Coecke to give a categorical axiomatization of Quantum Mechanics. Our aim in this introductory lecture is to explain the underlying logical paradigm, and the connections between logic, computation and categories, with particular emphasis on motivations from Quantum Informatics.
|
|
