;Nnews
Science | DOI: 10.1145/1831407.1831413
Alex Wright
Linear Logic
A novel approach to computational logic is reaching
maturity, opening up new vistas in programming languages,
proof nets, and security applications.

When the French lo- gician Jean-Yves Gi- rard first visited Xerox PARC during a trip to Silicon Valley in 1984,
he knew he was in the right place. See-
ing computer scientists collaborating
with linguists, ethnographers, and
other non-programmers, he started to
consider the possibilities of bridging
computer science with his own branch
of philosophy. “What impressed me
most was the change of spirit,” he re-
calls. “It was a very special time.”
Following his trip to California, Gi-
rard began work on his breakthrough
paper “Linear Logic,” which postulated
an entirely new approach to logic, one
deeply informed by computational
principles. In the ensuing years, the
principles of linear logic have found
their way into a broad range of other are-
nas including programming languages,
proof nets, security applications, game
semantics, and even quantum physics.

PhotograPh by anne Van der stegen

In the early 1980s, logicians like Girard were just starting to take an interest in computer science, while a handful of computer scientists were starting to recognize the potential of logical proof systems as a framework for functional programming. Linear logic represented an important step forward

french logician Jean-Yves Girard, author of the seminal paper “Linear Logic.”

for computer science because it chal-
lenged the conceptual limitations of
traditional classical logic. For thou-
sands of years, the study of logic had
hinged on the assumption of perma-
nent Aristotelian truths, or unchanging
essences. A was A, B was B, and would
ever be thus. Through the lens of com-
puter science, Girard began to see a way
out of this “foundational aphoria.” His
chief insight was that logic could func-
tion without this unspoken assumption
of perenniality. “This was a big shock,”
Girard recalls. “The discovery of linear
logic went completely against all the
things I had been taught in logic.”