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.