Professor Areski Nait Abdallah
Dept. Computer Science, University of Western Ontario
According to Niels Bohr "If you can fathom quantum mechanics without getting dizzy, then you don’t understand any of it." Logic is the art of organizing the elements of the discourse so that the conclusions clearly and obviously follow from the premisses.
Logical studies of quantum mechanics took off with the landmark 1936 quantum logic paper of Birkhoff and von Neumann, contemporary with the discovery of the foundations of computer science by Curry, Church and Turing. The needs of quantum based computing, and the discovery of the tight relation between computing and logic highlighted by Curry-Howard correspondence motivate a novel constructive logic based approach to some fundamental experiments of quantum mechanics. More specifically, we address single photon self-interference experiments and the related wave-particle duality paradox.
A. Church. The calculi of λ-conversion. Annals of Mathematical Studies. Princeton University Press, 1941
G. Birkhoff and J. von Neumann. The logic of quantum mechanics. Annals of Mathematics, 37:823–843, 1936.
P. Grangier, G. Roger, and A. Aspect. Experimental evidence for a photon anticorrelation effect on a beam splitter: a new light on single-photon interference.Europhys. Lett., 1:173, 1986.
W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.
M. A. Nait Abdallah. The logic of partial information. EATCS research monographs in theoretical computer science. Spinger Verlag, 1995.
M.A. Nait Abdallah. On an application of Curry-Howard isomorphism to quantum mechanics. in P. d’Aquino, Logic Colloquium ’12: Manchester,UK July 2012, BSL, pages 383–384, 2014.