HOL-CASL v0.42, 31 May 2000
Parser and Static Checker
Caution! This is an old version and is no longer supported.
The new version can be found here.
Features
The HOL-CASL parser and static checker supports following features:
-
Parsing of full CASL syntax (including libraries)
-
Static analysis of basic and (some) structured specifications
(excluding symbol maps)
-
Mixfix analysis
-
Formatting of specifications and libraries in LaTeX
The HOL-CASL parser and static checker is written in Standard ML,
using the Isabelle
parser.
Warning
This is an experimental prototype implementation!
See the list of known problems.
Installation
You can download a standalone version of the HOL-CASL Parser and static checker
(you do not need to install Standard ML!):
There exists a web
interface , where you can directly check your specification.
Old versions
of the HOL-CASL parser and static checker can be found here
Local installation
Lokale Installation für Benutzer mit Bremer Account
Contact: The HOL-CASL
Team (Kolyang, Till Mossakowski, Markus Roggenbach, Pascal Schmidt)