
Invited Talks
Invited Talks
Samson Abramsky
University of Oxford, UK
DEMONIC programming: a computational language for
singleparticle equilibrium thermodynamics, and its formal
semantics
Maxwell's Demon, ?a being whose faculties are so sharpened that
he can follow every molecule in its course', has been the centre of much
debate about its abilities to violate the second law of thermodynamics.
Landauer's hypothesis, that the Demon must erase its memory and incur a
thermodynamic cost, has become the standard response to Maxwell's dilemma,
and its implications for the thermodynamics of computation reach into many
areas of quantum and classical computing. It remains, however, still a
hypothesis. Debate has often centred around simple toy models of a single
particle in a box. Despite their simplicity, the ability of these systems
to accurately represent thermodynamics (specifically to satisfy the second
law) and whether or not they display Landauer Erasure, has been a matter
of ongoing argument. The recent NortonLadyman controversy is one such
example.
In this talk we present a programming language to describe these simple
thermodynamic processes, and give a formal operational semantics and
program logic as a basis for formal reasoning about thermodynamic systems.
We formalise the basic singleparticle operations as statements in the
language, and then show that the second law must be satisfied by any
composition of these basic operations. This is done by finding a
computational invariant of the system. We show, furthermore, that this
invariant requires an erasure cost to exist within the system, equal to kT
ln 2 for a bit of information: Landauer Erasure becomes a theorem of the
formal system. The NortonLadyman controversy can therefore be resolved
in a rigorous fashion, and moreover the formalism we introduce gives a set
of reasoning tools for further analysis of Landauer erasure, which are
provably consistent with the second law of thermodynamics.
Adam Whiteside
University of Melbourne, Australia and Google
Classical Problems to Make Quantum Computing a Reality
Recent experiments have shown exciting progress toward creating
reliable quantum bits (qubits) that will make up tomorrow's quantum
computers. While experiments and engineers continue to make the physical
side a reality, computer scientists and software engineers will be
essential to getting the most out of such expensive hardware. An entire
stack of classical software must be developed, requiring creative
solutions to a broad range of problems. We provide an introduction to
quantum computing and an overview of the problems left to face in an
effort to inspire more research in these important areas.



