HOL-CASL is outdated now! Please use the Heterogeneous Tool Set.

Welcome to the HOL-CASL home page!

This work is a part of the Common Framework Initiative.

What is HOL-CASL?

HOL-CASL is a theorem proving system for CASL. It is based on the generic theorem prover Isabelle.
HOL-CASL uses the CASL tool set (CATS) to analyse and encode a CASL library.

New features of release 0.85:

free (=inductively defined) predicates are supported.
partial constructors in generated types are supported.
default simplifier set has been improved.
better library management.
part of the basic datatypes have been verified within HOL-CASL!

Documentation

Installation

Mailing list

Related Systems

See the CoFI tools home page.

Bibliography

Till Mossakowski, Kolyang, Bernd Krieg-Brückner: Static semantic analysis and theorem proving for CASL. 12th Workshop on Algebraic Development Techniques, LNCS.

Abstract

postscript file

gzip'ed postscript file

Till Mossakowski: CASL - From Semantics to Tools. TACAS 2000.
Abstract, postscript file and gzip'ed postscript file

Till Mossakowski: Relating CASL with Other Specification Languages: the Institution Level. Theoretical Computer Science, to appear.
Abstract, postscript fileand gzip'edpostscript file

Contributors

Different colleagues from CoFI have participated through various discussions to this work. They deserve our warmest thanks.

Contact Address

cofi@Informatik.Uni-Bremen.DE