% README for Lolli 0.701 -- Josh Hodas (hodas@saul.cis.upenn.edu) 11/30/92*

This distribution contains the files necessary to build an interpreter for
a prolog-like language based on intuitionistic linear logic.

The language Lolli (named for the linear logic implication operator "-o"
called lollipop), is a full implementation of the language described in
our paper "Logic Programming in a Fragment of Intuitionistic Linear
Logic" (Hodas & Miller, to appear in Information and Computation '92), 
though it differs a bit in syntax, and has several built-in extra-logical 
predicates and operators.**

This preliminary implementation was developed over the last year 
and is based on code written by Frank Pfenning and Conal Elliot for their 
excellent paper "A Semi-Functional Implementation of a Higher-Order Logic 
Programming Language" which appears in "Topics in Advanced Language 
Implementation" , MIT Press, Peter Lee editor.  The paper is also available 
from CMU as Ergo Report 89-080. 

The system is written in Standard ML of New Jersey, and the parser and lexer
were built using the parser-generator (MLYACC) and lexical-analyzer-generator
(MLLEX) distributed with that system.  Though source files for the parser 
and lexer have been included, the parser and lexer have already been built, 
so you do not need access to the MLYACC or MLLEX.

For those who do not have SML-NJ at their site, I am attempting to provide
pre-built binaries for a variety of architectures. These binaries will
be stored in compressed form in the same directory (/pub/lolli) from
which you ftp'ed this distribution. At present Sparc and NeXT binaries
are available.  If you compile lolli on a new architecture, please contact me
so that I can distribute your binary.



Contents of the Distribution
----------------------------

The ./src directory contains files used to build an executable version
of Lolli using SML-NJ. It also contains the following two subdirectories
which hold the source code for the system itself.

    ./src/parser contains the source grammar and lex files used to 
    build the Lolli parser, as well as the code used to interface the 
    parser to the main system.

    ./src/interpreter includes all the SML source code for the Lolli 
    interpreter itself. The core of the prover is in 
    ./src/interpreter/interprter.sml. The remaining files define the 
    term and formula language, and give code for lifting terms to formulas.

The ./papers directory includes DVI and PostScript versions of several
papers relating to Lolli, as well as a preliminary version of the 
Elliot & Pfenning paper mentioned above.

The ./examples directory includes several sub-directories of example Lolli
programs. Most are drawn from the papers mentioned above, but almost all
have been changed to make use of some of the built-in predicates, to make them
more functional.


--------------------
*Work on this project, by Josh Hodas and Dale Miller, has been funded by
ONR N00014-88-K-0633, NSF CCR-87-05596, NSF CCR-91-02753, and DARPA 
N00014-85-K-0018, through the University of Pennsylvania.  Miller was also 
supported by SERC Grant No. GR/E 78487 "The Logical Framework" and ESPRIT 
Basic Research Action No. 3245 "Logical Frameworks: Design Implementation 
and Experiment" while he was visiting the University of Edinburgh.


**The internal representation of formulas and proof contexts is
actually based on an earlier version of the logic, described in the
"extended abstract" version of the paper presented at the 1991 Logic
In Computer Science conference (which paper is also include in this
distribution). This distinction permeates aspects of the interpreter
in subtle ways, but should not be apparent to the user. A future
version of the system will likely shift to an internal representation
more in line with the journal version of the paper.

More seriously, the interpreter implements a modified proof system that
handles "TOP" lazily, rather than generating all possible subcontexts.
A Latex file of the modified proof system is in the ./papers directory.
The proof that it is sound and complete relative to the original system 
has been completed, and will appear in my thesis.