Whereas classical logic might support an assertion like type A → B, computer programs require a set of concrete instructions for transforming A into B, such as applications, variables, or exception handlers. In the eyes of a computer program, then, A is not a permanent entity but a consumable resource. To address this problem, Girard proposed a resource-conscious approach to logic, laying out an entirely new framework capable of describing resources that could be used and depleted during the course of an operation.

In the nearly quarter of a century since Girard published his seminal paper, most of the foundational theoretical work in linear logic has been completed. However, computer scientists continue to find new applications of the theory across a wide range of disciplines like proof nets, categorical semantics, and computer security applications.

At Carnegie Mellon University (CMU), computer science professor Frank Pfenning has been exploring the application of linear logic to distributed security problems. After one of his students introduced him to linear logic, he became convinced it provided the ideal conceptual framework for specifying difficult-to-encode rules like complex privacy policies or resource conservation strategies. “I was most interested in characterizing, logically, complex properties of distributed systems,” Pfenning explains.

Working with a team of students, he used the principles of linear logic

“the discovery
of linear logic went
completely against
all the things i had
been taught in
logic,” says
Jean-Yves Girard.

to implement a proof-carrying file sys-
tem (PCFS), featuring an access con-
trol policy that is stated as a logical
theory, wherein file access is granted
on the condition of a logical proof of
policy compliance. “Linear logic is tre-
mendously useful here,” he explains,
“because we can easily represent the
change of state that takes place, for ex-
ample, when you read or write a file.”
Working with Symantec, Pfenning
and CMU postdoctoral researcher
Deepak Garg have applied PCFS to for-
malize the access control policies of
the national intelligence community in
the United States. In collaboration with
Jamie Morgenstern, an undergraduate
student from the University of Chicago,
Pfenning is now working on extending
the implementation to handle even
more complex policies. Pfenning feels
the biggest challenges lie in translating
complex real-world rule sets into un-
ambiguous logic. The ideal outcome is
what he calls “an abstract logical form
that is theoretically tractable and at the
same time practically useful.”

Proof nets

Linear logic has also opened new doors in the field of proof nets. Prior to the introduction of linear logic, most computer scientists working in the field relied on intuitionistic logic, following the well-established Curry-Howard Correspondence, which suggested that formal proof calculi shared a common structure with computational models. Before the advent of linear logic, this model had served as the de facto standard for types. “Linear logic enriched this world greatly,” says Dale Miller, director of research at INRIA Saclay, who has spent the last several years applying the principles of linear logic to proof systems.

“Originally, proof systems were used to build ‘big-step’ inference rules from the ‘small-step’ inference rules of linear logic,” Miller explains. Now, he is exploring the possibilities of so-called focused proof systems by using those “small-step” inference rules to build a range of proof systems for classical and intuitionistic logic. “If one has an interpreter for focused linear logic, that interpreter can be used as an interpreter for many proof systems,” says Miller, citing the examples of emulating sequent calculus and tableaux. “Different choices yield different and

Obituary

Nicolas Georganas, Multimedia Guru, Dies at 67

nicolas D. Georganas, a leader in multimedia networking, died on July 27 at age 67. Georganas was founding editor-in-chief, in 2004, of ACM Transactions on Multimedia Computing, Communications, and Applications (ACM TOMCCAP). he promoted the linking of video, audio, and other sensory input—lately focusing on haptics—for a wide variety of distributed interactive systems, from telemedicine to high-level gaming to security.

“he is one of the godfathers of
multimedia,” says ralf Steinmetz,
editor-in-chief of ACM TOMCCAP
and adjunct professor at
technical University Darmstadt.
“whatever we did in this area,
particularly with AcM, he was
from the beginning involved in it.”
“he was incredibly kind
and very friendly,” says Klara
nahrstedt, a computer science
professor at the University of
illinois at Urbana-champaign,
who described Georganas as an
elder statesman in a young field.
“he truly served many people as
a mentor.”
Born and educated in
Athens, Greece, Georganas
earned a Ph. D. in electrical
engineering at the University
of Ottawa, where he served on
the faculty from 1970 until his
death. Georganas’ research
contributions included ambient
multimedia intelligence systems,
multimedia communications,
and collaborative virtual
environments. he published
more than 425 technical papers
and is co-author of Queueing
Networks—Exact Computational
Algorithms: A Unified Theory by
Decomposition and Aggregation.