Communications - October 2010

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.

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.