
15816 Linear Logic
Projects
This page contains some suggestions for projects for this course. You
are encouraged to draw upon your own experience and judgment to develop
other project ideas. Note that the given references are by no means
exhaustive, but provide an entry point to the literature.
Warning:
The links to papers have not yet been checked for accuracy.
A project might consist of some theoretical analysis, an
implementation, or an encoding or explanation using linear or other
substructural logic. The only constant requirement is that the project
contain a term paper that explains the background, motivation, technical
contribution, and draws some conclusion. I would expect the term papers
to be at least about 10 pages long. The best term papers may be
suitable for publication, depending on the chosen topic and results.
Foundations
Classical Linear Logic
Give a judgmental explanation of linear logic in terms of three basic
judgments: A is true, A is false, and contradiction. We have
unrestricted and linear assumptions about the truth and falsehood of
propositions, and our only goal is to derive a contradiction. From this
we might be able to see clearly how intuitionistic linear logic is a
generalization of classical linear logic by accomodating other goals
besides contradiction. It might also be interesting to see if one can
join both classical and intuitionistic logic consistently in the same
system.

J.Y. Girard.
Linear logic.
Theoretical Computer Science, 50:1102, 1987.

JeanMarc Andreoli.
Logic programming with focusing proofs in linear logic.
Journal of Logic and Computation, 2(3):197347, 1992.
Intuitionistic Focusing
Prove the soundness and completeness of rules for intuitionistic
focusing, following Andreoli's seminal paper. One might also consider
further refinement of focusing, for example, through a better treatment
of unrestricted assumptions.

JeanMarc Andreoli.
Logic programming with focusing proofs in linear logic.
Journal of Logic and Computation, 2(3):197347, 1992.
Unrestricted, Affine, Strict, and Linear Logic
Develop and prove the interesting properties of various translations
between unrestricted, affine, strict, and linear logic. The structure
of proof changes during the translations would be of particular
interest.

K. Dosen.
Modal translations in substructural logics.
Journal of Philosophical Logic, 21:283336, 1992.
Temporal and Linear Logic
Both temporal and linear logic have a notion of state. In temporal
logic, we reason unrestrictedly within a world (= state) and have modal
operators that transport us to other world. In linear logic the very
definition of truth talks about whether a goal can be achieved from some
resources, not if it is true in the current state. Consider one or more
possible ways temporal and linear logic might be combined.
Implementation
GoalDirected Theorem Proving
Implement a goaldirected theorem prover for linear logic exploiting
focusing and unification where appropriate. Test this prover on
examples such as planning as used in class.
Inverse Method Theorem Proving
Develop an inverse method theorem prover that takes advantage of
focusing and a sequent calculus with multiple zones designed to reason
from the initial sequents to the conclusion. Test this prover on
examples such as planning as used in class.

Grigori Mints.
Resolution calculus for the first order linear logic.
Journal of Logic, Language and Information, 2:5893, 1993.

T. Tammet.
Proof strategies in linear logic.
Journal of Automated Reasoning, 12:273304, 1994.
Also available as Programming Methodology Group Report 70, Chalmers
University, 1993.
Available in PostScript format.
The source code for the theorem provers is available as a
TAR file.
ModelChecking Linear Logic
Isolate useful fragment of linear logic, such as multiplicative
exponential linear logic, for which theorem proving is decidable and
develop a decision procedure following techniques for model checking
(e.g., using SAT or BDDs). Apply to encodings which fall into this
class.

E.M. Clarke, Orna Grumberg, and Doron Peled.
Model Checking.
MIT Press, Cambridge, Massachusetts, 1999.

Henry A. Kautz and Bart Selman.
Unifying satbased and graphbased planning.
In T. Dean, editor, Proceedings of the 16th International Joint
Conference on Artifical Intelligence (IJCAI'99), pages 318325, Stockholm,
Sweden, July 1999. Morgan Kaufmann.
Substructural Functional Programming
Implement a functional language with strict, linear, or affine types.
This language should have sufficient expressive power power (say,
include recursion and recursive types) to allow experimentation with
examples and optimizations suggested by the use of substructural types.

P. Wadler.
Linear types can change the world.
In M. Broy and C. B. Jones, editors, IFIP TC 2 Working
Conference on Programming Concepts and Methods, pages 561581, Sea of
Gallilee, Israel, April 1990. NorthHolland.
Available in PostScript format.

Martin Hofmann.
Linear types and nonsize increasing polynomial time computation.
Theoretical Computer Science, 2000.
To appear. A previous version was presented at LICS'99.
Available electronically.

Martin Hofmann.
A type system for bounded space and functional inplace update.
Nordic Journal of Computing, November 2000.
To appear. A previous version was presented as ESOP'00.
Available electronically.

Klaus Aehlig and Helmut Schwichtenberg.
A syntactical analysis of nonsizeincreasing polynomial time
computation.
Submitted, 2001.
A previous version presented at LICS'00.
Available electronically.
Concurrent Linear Programming
Implement a fragment of linear logic as a concurrent logic programming
language. Try to identify a fragment of linear logic large enough so a
number of our encodings of process calculi can be written out and
executed (albeit slowly).

J.M. Andreoli, L. Leth, R. Pareschi, and B. Thomsen.
True concurrency semantics for a linear logic programming language
with broadcast communication.
In M.C. Gaudel and J.P. Jouannaud, editors, Proceedings of
International Joint Conference on Theory and Practice of Software
Development, pages 182198, Orsay, France, April 1993. SpringerVerlag LNCS
668.
Available in PostScript format.
Linear Concurrent Constraint Programming
Give a highlevel implementation of the linear concurrent constraint
programming paradigm.

François Fages, Paul Ruet, and Sylvain Soliman.
Linear concurrent constraint programming: Operational and phase
semantics.
Information and Computation, 165(1):1441, 2001.
Available electronically.
Applications
Concurrent and Mobile Programming
Develop the techniques we employed to model the picalculus to model
other calculi such as the Join Calculus, Mobile Ambients, or CML. Give
precise statements of the adequacy of the representation and prove
correct if feasible.
Games
One of the driving intuitions behind the semantics of linear logic as
been the notion of a game. Apply the techniques we have developed to
describe some game(s) (either in the ordinary sense of the word, or in
the sense of game theory) in linear logic.

Y. Lafont and T. Streicher.
Games semantics for linear logic.
In Sixth Symposium on Logic in Computer Science, pages 4350.
IEEE Computer Society Press, July 1991.
Amsterdam, The Netherlands.

S. Abramsky and R. Jagadeesan.
Games and full completeness for multiplicative linear logic.
Journal of Symbolic Logic, 59(2):543574, 1994.
Available
PostScript format.
Constraint Handling Rules
Constraint Handling Rules (CHR) provide a highlevel notation to
specify and implement constraint solvers such as unification, Boolean
constraint simplification, or Gaussian elimination. Represent CHR in
linear logic in such a way that it is plausible to execute them, perhaps
following a logic programming semantics.

Thom Früwirth.
Theory and practice of constraint handling rules.
Journal of Logic Programming, 17(13):95138, October 1998.
Programming Languages with Effects
Consider various functional or logic programming languages with
effects (mutable references, exception, input, output) and consider how
they can be represented at a high level of abstraction using either
linear logic or a linear logical framework.

Jawahar Lal Chirimar.
Proof Theoretic Approach to Specification Languages.
PhD thesis, University of Pennsylvania, May 1995.
Available in PostScript format.

Iliano Cervesato and Frank Pfenning.
A linear logical framework.
Information and Computation, 1998.
To appear in a special issue with invited papers from LICS'96, E.
Clarke, editor.
Available in PostScript format.
[ Home
 Schedule
 Assignments
 Handouts
 Software
 Resources
]
fp@cs
Frank Pfenning
