often, known proof systems.”
In recent years, linear logic has also
given rise to a new genre of program-
ming languages like Forum, Lolli, and
Lygon that incorporate richer forms of
expression to allow more powerful ap-
proaches to proofs.
Looking ahead, Pfenning believes
there is still work to do in improving
the state of automation in linear log-
ic. “We need theorem provers, model
checkers, and other tools for working
with linear logic to make its applica-
tion to real-world problems easier.”
Miller agrees that linear logic has the
potential to support the automation
of theorem proving. “Focused proof
systems give a central role to inference
rules that are invertible,” he explains.
“When a formula is introduced by an
invertible rule, that formula can be dis-
carded. Such information is useful in
building theorem provers.”
Miller also sees an opportunity to
use linear logic and proof search to
provide specifications of algorithms,
using proof theory research to help
in reasoning about such algorithmic
specifications. He also hopes to see the
day when a large “logic of unity” might
take shape that would encompass clas-
sical, intuitionistic, and linear logic in
one grand system.
Where could linear logic go from
here? Other active research areas include concurrency theory, quantum
computing, game semantics, implicit
computational complexity, and the verification of imperative programs with
heaps using separation logic, a close
cousin of linear logic.
With the field maturing, the funda-
mental principles of linear logic are re-
ceding into the background as an area
of active inquiry as computer scientists
learn to apply the established princi-
ples to emerging computational prob-
lems. “Linear logic is no longer alive as
a specific subject in which you work,”
says Girard. “It’s become something
classical. It is part of the toolbox.”
Pfenning agrees with Girard’s as-
sessment, but thinks linear logic lacks
the widespread exposure it deserves
at every level of the computer science
curriculum. “It should be part of the
standard toolkit,” he says, “but I don’t
think it is taught in enough places right
now, especially in the United States.”
Girard, meanwhile, has moved on
active research
areas for linear
logic include
concurrency theory,
quantum computing,
game semantics,
and implicit
computational
complexity.
from the problems of computing to set
his sights on more esoteric quanda-ries. “I would like to understand why
certain things are difficult, why the
world is not transparent,” he says. Alas,
perhaps some questions are better left
to logicians.
Further Reading
Abramsky, S., Jagadeesan, R., and Malacaria, P.
Full abstraction for PCF (extended abstract).
Lecture Notes in Computer Science 789,
Proceedings of Conference on Theoretical
Aspects of Computer Software, 1994.
Bowers, K.D., Bauer, L., Garg, D., Pfenning, F.,
and Reiter, M.K.
Consumable credentials in logic-based
access-control systems. Proceedings of
the 14th Annual Network and Distributed
System Security Symposium, San Diego, CA,
Feb. 28–March 2, 2007.
Girard, J.-Y.
Linear logic. Theoretical Computer Science
50, 1, 1987.
Lincoln, P., Mitchell, J., Scedrov, A.,
and Shankar, N.
Decision problems for propositional linear
logic. Proceedings of the 31st Annual
Symposium on Foundations of Computer
Science, St. Louis, MO, Oct. 22-24, 1990.
Miller, D.
An overview of linear logic programming.
Linear Logic in Computer Science, Ehrhard,
T., Girard, J.-Y., Ruet, P., and Scott, P. (Eds.),
Cambridge University Press, London, U.K.
2004.
Alex Wright is a writer and information architect who
lives and works in brooklyn, ny. Patrick Lincoln, sri
international, contributed to the development of this
article.
© 2010 acM 0001-0782/10/1000 $10.00
Milestones
CS Awards
neVanLinna PRize
Daniel Spielman, a professor of
computer science and applied
mathematics at Yale University,
won the rolf nevanlinna Prize,
one of the highest honors in
the field of mathematics, from
the international Mathematical
Union. the nevanlinna Prize
recognizes researchers under
the age of 40 for “outstanding
contributions in mathematical
aspects of information science.”
Spielman’s research has
included smoothed analysis
of linear programming,
algorithms for graph-based
codes, and applications of
graph theory to numerical
computing.
“the same way that
physicists grow up dreaming
about winning the nobel Prize,
i’ve dreamed of winning the
nevanlinna Prize ever since
i was a graduate student,”
Spielman said in a statement.
“i was in shock when lászló
lovász, the president of the
international Mathematical
Union, called me up to tell me
that i had won. i had to hear
him say it a few times before i
believed him. it is an incredible
honor. Many of my heroes have
won this prize.”
micRoSoft a WaRD
cheryl Arnett from Sunset
elementary School in craig,
cO, and rawya Shatila from
Maskassed Khalil Shehab
School in Beirut, lebanon,
won first place in the 2010
U.S. innovative education
Forum, a Microsoft-sponsored
competition for teachers
who use technology in their
curriculum to improve
student learning. Arnett and
Shatila’s joint project, called
“Digital Stories: A celebration
of learning and culture,”
connected Arnett’s class of
first- and second-graders in
craig, cO, to Shatila’s second-graders in Beirut. the two
teachers, who had never met
prior to their collaboration,
used wikis, blogs, and online
mapping tools to share stories
and activities to help students
increase their global awareness
of the similarities and
differences between children
from different nations. Arnett
and Shatila will represent the
United States at the worldwide
innovative education Forum in
South Africa this fall.
—Jack Rosenberger