New Release of HOL-CASL parser and checker

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear friends,

release 0.3 of the HOL-CASL parser and checker is now available at

http://www.informatik.uni-bremen.de/~cofi/CASL/parser/parser.html

The main new features are

Basic specifications
- The parser covers all annotations mentioned in the Summary
- Precedence and associativity annotations have the desired effect

Structured specifications
- Renamings and revealings are statically checked,
  but only without qualifications
- Instantiations are statically checked in a rudimentary form

Libraries
- A rudimentary treatment of libraries (using PATHs) is available
- The basic datatypes can be accessed with
    from Basic/xxx get yyy
  without the need to re-load them; this saves time
  (You can disable this feature, e.g. if you want to compile
   the basic datatypes themselves)

ATerms
- Abstract syntax trees can be fed into the static checker,
  using the ATerm format. Thus, you can combine the static
  checker with other parsers.
- The global environment can be stored in the ATerm format.
  This should ease the translation of CASL to other theorem
  proving or rewriting tools.
  However, note that the global environment written in ATerm
  format becomes very large! We should discuss how this can be
  made shorter. For the moment, you can use the -e option
  to switch off the output of the global environment in
  ATerms format. We provide another, more text-based
  format (xxx.env) which is considerably shorter.

Greetings,
Till
-----------------------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3550
University of Bremen            till@informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------