Lygon: Logic Programming with Linear Logic

Key Resource
Links2Go Key Resource
Logic Topic

Lygon is a logic programming language that is based on linear logic. It can be viewed as Prolog extended with features derived from linear logic. These features include a declarative notion of state and the ability to express problems involving concurrency. Also, the availability of use once predicates allows simple solutions to problems such as graph manipulation. Although the design of Lygon relies on a delicate proof-theoretic analysis of linear logic, programmers need have no knowledge of proof theory.

Linear logic can be used to model the consumption of resources. Whereas clauses in Prolog, based on classical logic, can be used many times during the execution of a program, clauses in Lygon, based on linear logic, must (by default) be used exactly once. Since both classical and intuitionistic logic can be embedded in linear logic, Lygon generalizes pure Prolog. Indeed, pure Prolog code (Edinburgh syntax) can be executed by Lygon's interpreter.

A description of Lygon, including design, implementation and applications, can be found in technical report 96/36: Hitch Hiker's Guide to Lygon 0.7. It is also available in postscript and pdf formats.


Linear logic has numerous applications in computing science, including natural language processing, concurrency, logic programming and resource management (for example garbage collection).

Lygon has a wide range of applications including graph problems (such as path-finding and Hamiltonian cycles), concurrent programming, modelling state, representing actions (e.g., the Yale shooting problem) and agent-oriented programming.

Current and Future Work

We have recently begun looking at applications of Lygon to agent-oriented systems. Since Lygon is suitable for concurrent programming, modelling actions, representing states and searching, it is natural to use Lygon for working with agent-oriented systems. This work is continuing.

Another thread of research concerns bottom-up computation. Most logic programming languages, and all known logic programming languages based on linear logic, use top-down computation. That is, a computation begins with a goal and seeks to prove it using the program. In bottom-up computation, we start with a program and seek to determine what goals will succeed from this program.  In classical logic, the bottom-up computation mechanism is used, for example, by deductive databases. Our current work in this area is foundational: identifying a calculus of bottom-up computation in linear logic (and in BI, the logic of bunched implications, developed by David Pym and Peter O'Hearn), and ensuring that the calculus satisfies various desirable properties.


Lygon grew out of some work on the proof-theoretic foundations of logic programming languages. The fundamental idea behind Lygon is the completeness properties of certain kinds of proofs in the linear sequent calculus, and the initial work in this area was done in the second half of 1990 (in Edinburgh and Melbourne). Over the next two years, the operational model of the language was defined, revised, extended and, in part, applied to other logics, and the language received its name over dinner one night late in 1992.

The first Lygon implementation appeared in the following year, although there were still some technical problems with the operational semantics, which were ironed out in early 1994, and a prototype implementation was completed later that year. Subsequently, the Lygon implementation was refined and extended, including a debugger and a graphical user interface.

The Name

Lygon St. is close to Melbourne University and is known for its restaurants and cafes. Lygon Rd., is close to Edinburgh University's then Computer Science Department.


Lygon is the work of a number of people. People currently working on Lygon include James Harland ( and David Pym (, who designed the language, and Michael Winikoff (, who implemented the language. The Lygon debugger was designed and implemented by Yi Xiao Xu (formerly at RMIT).

The Lygon Implementation

The Lygon implementation is freely available. As noted in the Lygon manual you will need a BinProlog executable. To use the GUI, you will also need to have installed TCL/Tk. The Lygon distribution is available as a gzipped tar file (24K) which includes examples.


The earliest Lygon-related publication was in 1991. It identified a notion of uniformity which was used to derive a class of formulae which could be considered to be a logic programming language. The paper also sketched a suitable resolution rule.
J. Harland and D. Pym, The Uniform Proof-theoretic Foundation of Linear Logic Programming (Extended Abstract), Proceedings of the International Logic Programming Symposium 304-318, San Diego, October, 1991 (gzipped postscript)
This foundational work was extended in a number of subsequent papers culminating in a journal article appearing in 1994 which presented a detailed analysis leading to a suitable class of formulae, a resolution rule, a completeness proof, and some ideas for the implementation of the resulting language.
D. Pym and J. Harland, A Uniform Proof-theoretic Investigation of Linear Logic Programming, Journal of Logic and Computation 4:2:175-207, April, 1994. (gzipped postscript)
The theoretical foundation having been set, attention turned to implementing the language and to the language's applications. The general development of the language was documented in a number of conference publications at ACSC. A discussion of the issues involved in implementing Lygon was presented at ILPS'95.
M. Winikoff and J. Harland, Implementing the Linear Logic Programming Language Lygon, Proceedings of the International Logic Programming Symposium (ILPS) 66-80, December, 1995. (gzipped postscript, pdf; presentation slides: pdf, postscript)

M. Winikoff and J. Harland, Deterministic resource management for the linear logic programming language Lygon, Technical Report 94/23, Melbourne University, 1994. (postscript)

A description of Lygon together with a discussion of its applications was presented at AMAST'96.

J. Harland, D. Pym and M. Winikoff, Programming in Lygon: An Overview, Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology (AMAST) 391-405, July, 1996. (gzipped postscript, pdf; presentation slides: pdf)
The Hitch Hiker's Guide to Lygon, a technical report, is more pragmatic: it contains directions for installing the Lygon implementation, a programmer-oriented description of the Lygon language and its semantics, and examples of Lygon's applications.
Michael Winikoff, Hitch Hiker's Guide to Lygon 0.7, Technical Report 96/36, Melbourne University, 1996. (postscript, pdf, html)
The above list of publications isn't complete. Other Lygon related publications can be found in Michael's publications page, James' publications page and David's publications page.

Student Projects

Over the last few years, several students have done projects which either contributed to, or used, Lygon. These projects include:

Other linear logic programming languages and related links

(Some of these links were copied from the LLP page).

Maintainers: James Harland, David Pym, Michael Winikoff /,, / Last updated: Wed 5 Jan 2000 / Department of Computer Science