Reversible and Quantum Computing

Why?

For a computer scientist, the interest in reversible and quantum computing can be summarized in the following thesis:

The discipline of computer science is founded on the "wrong worldview," a worldview that is fundamentally at odds with physical reality.

More than thirty years ago, Toffoli (1980) stated the following:

Mathematical models of computation are abstract constructions, by their nature unfettered by physical laws. However, if these models are to give indications that are relevant to concrete computing, they must somehow capture, albeit in a selective and stylized way, certain general physical restrictions to which all concrete computing processes are subjected.

More recently, Girard (2007) states:

In other terms, what is so good in logic that quantum physics should obey? Can't we imagine that our conceptions about logic are wrong, so wrong that they are unable to cope with the quantum miracle? ... Instead of teaching logic to nature, it is more reasonable to learn from her. Instead of interpreting quantum into logic, we shall interpret logic into quantum.

There is a growing research programme that accepts the quantum reality as foundational and investigates its consequences. This class is an introduction to this growing and exciting research area.

Office hours

Amr: 9am-12pm Wednesdays and by appointment.

Schedule of Talks

Feb. 3: Rebecca: Functional Quantum Programming (Mu and Bird)

Feb. 8: Adam: Shor in Haskell: the Quantum IO Monad (Alexander S. Green and Thorsten Altenkirch)

Feb. 10: Mike: Thermodynamics (Maxwell, Landauer, Bennett)

Feb. 15: Devarshi: Linear Logic (Wadler)

Mar 1: Hongyan: An injective language for reversible computation (Shin-Cheng Mu, Zhenjiang Hu, and Masato Takeichi)

Mar 3: JP: Hilbert spaces

Mar 8: Eran: Time and space complexity

Mar 10: Will: Reversible Logic (Toffoli)

Eric: Categorical Quantum Mechanics (Abramsky and Coecke)

Jason: Quantum Lambda Calculus (Selinger and Valiron)

Josh: Linear Logic (Girard)

Background Reading

Logical Reversibility of Computation, Charles H. Bennett.
Notes on Landauer's Principle, Reversible Computation, and Maxwell's Demon, Charles H. Bennett.
Notes on the History of Reversible Computation, Charles H. Bennett.
Conservative Logic, Edward Fredkin and Tommaso Toffoli.
Reversible Computing, Tommaso Toffoli.
Linear Logic, Jean-Yves Girard.
Linear Logic: Its Syntax and Semantics, Jean-Yves Girard.
A Syntax for Linear Logic, Philip Wadler.

Advanced Material

Linear Logic and Permutation Stacks-- The Forth Shall Be First, Henry G. Baker.
NREVERSAL of Fortune --- The Thermodynamics of Garbage Collection, Henry G. Baker.
From Reversible to Irreversible Computations, Alexander S. Green and Thorsten Altenkirch.
Logical Reversibility, Paolo Zuliani
Using Forth in an Investigation into Reversible Computation, Bill Stoddart.
An Injective Language for Reversible Computation, Shin-Cheng Mu, Zhenjiang Hu, and Masato Takeichi.
Reversible Simulation of Irreversible Computation, Ming Li, John Tromp, and Paul Vitanyi.
Time and Space Bounds for Reversible Simulation, Harry Buhrman, John Tromp, and Paul Vitanyi.
Quantum Theory, the Church-Turing Principle, and the Universal Quantum Computer, David Deutsch.
Functional Quantum Programming, Shin-Cheng Mu and Richard Bird.
A Functional Quantum Programming Language, Jonathan J. Grattage.
Quantum Lambda Calculus, Peter Selinger and Benoit Valiron.
A Lambda Calculus for Quantum Computation with Classical Control, Peter Selinger and Benoit Valiron.
Shor in Haskell: The Quantum IO Monad, Alexander S. Green and Thorsten Altenkirch.
Structuring Quantum Effects: Superoperators as Arrows, Juliana K. Vizzotto, Thorsten Altenkirch, and Amr Sabry.
A Categorical Semantics of Quantum Protocols, Samson Abramsky and Bob Coecke.
Types for Quantum Computing, Ross Duncan.

Optional Material

Program Inversion, Edsger W. Dijkstra.
Linear Programs in a Simple Reversible Language, Armando B. Matos.
Principles of a Reversible Programming Language, Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Gluck.
Revisiting an Automatic Program Inverter for Lisp, Robert Gluck and Masahiko Kawabe.
Reversible Computation and Reversible Programming Languages, Tetsuo Yokoyama.
Running Programs Backwards: the Logical Inversion of Imperative, Brian J. Ross.
A Reversible SE(M)CD Machine, Werner Kluge.
A Logically Reversible Evaluator for the Call-by-name Lambda Calculus, Lorenz Huelsbergen.
There and Back Again: Arrows for Invertible Programming, Artem Alimarine, Sjaak Smetsers, Arjen van Weelden, Marko van Eekelen, and Rinus Plasmeijer.
Reversible Communicating Concurrent Systems, Vincent Danos and Jean Krivine.
General Reversibility, Vincent Danos, Jean Krivine, and Pawel Sobocinski.
Formal Molecular Biology done in CCS-R, Vincent Danos and Jean Krivine.
A Structural Approach to Reversible Computation, Samson Abramsky.
Reversible Combinatory Logic, Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky.
Quantum Computation by Adiabatic Evolution, Edward Farhi, Jeffrey Goldstone, Sam Gutmann, and Michael Sipser.
Physics, Topology, Logic and Computation: A Rosetta Stone, John C. Baez and Mike Stay.
Universality Issues in Reversible Computing Systems and Cellular Automata, Kenichi Morita.
Boomerang: Resourceful Lenses for String Data, Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, and Alan Schmitt.