Lightweight Java (LJ)
=====================

Information about LJ
--------------------
Please see the Isabelle-generated PDF and/or

    http://rok.strnisa.com/lj/


Overview of files
-----------------

├── IsaMakefile  ("Isabelle makefile to verify the theories, and to
                   create a PDF within the 'document' directory.")
├── Lightweight_Java_Definition.thy   ("The Ott-generated Isabelle2011
                                        definition of LJ.")
├── Lightweight_Java_Equivalence.thy  ("Some equivalence functions based
                                        on the definition.")
├── Lightweight_Java_Proof.thy        ("A type soundness proof for LJ.")
├── README  ("This file.")
├── ROOT.ML  ("A file directing Isabelle which theories to compile.")
├── config  ("AFP maintenance configuration file.")
├── document
│   ├── root.bib  ("BibTeX bibliography for the 'root.tex'.")
│   └── root.tex  ("LaTeX source for generating the PDF overviewing LJ.")
└── ott-src  ("LJ's Ott source files provided for reference.")
    ├── Makefile
    ├── README
    ├── lj.ott
    ├── lj.tex
    ├── lj_base.ott
    └── lj_common.ott


Maintaining LJ
--------------

- Lightweight_Java_Definition.thy

Since "Lightweight_Java_Definition.thy" is generated by Ott, it should _not_
be modified directly. Please either:

1) E-mail the main author (rok@strnisa.com) to sort out any problem; or,

2) Modify the provided Ott-source files to obtain the desired result. Please
   notify the main author (rok@strnisa.com) of any such changes.


- Lightweight_Java_Equivalence.thy and Lightweight_Java_Proof.thy

These two files can be modified at will, as long as the semantics of "progress"
and "wf_preservation" is preserved.