15-816 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:1-102, 1987.
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197-347, 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.

Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197-347, 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:283-336, 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

Goal-Directed Theorem Proving

Implement a goal-directed 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:58-93, 1993.
T. Tammet. Proof strategies in linear logic. Journal of Automated Reasoning, 12:273-304, 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.

Model-Checking 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 sat-based and graph-based planning. In T. Dean, editor, Proceedings of the 16th International Joint Conference on Artifical Intelligence (IJCAI'99), pages 318-325, 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 561-581, Sea of Gallilee, Israel, April 1990. North-Holland. Available in PostScript format.
Martin Hofmann. Linear types and non-size 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 in-place 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 non-size-increasing 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 182-198, Orsay, France, April 1993. Springer-Verlag LNCS 668. Available in PostScript format.

Linear Concurrent Constraint Programming

Give a high-level 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):14-41, 2001. Available electronically.

Applications

Concurrent and Mobile Programming

Develop the techniques we employed to model the pi-calculus 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 43-50. 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):543-574, 1994. Available PostScript format.

Constraint Handling Rules

Constraint Handling Rules (CHR) provide a high-level 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(1-3):95-138, 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.

fp@cs
Frank Pfenning

15-816 Linear Logic Projects