| Publication type: |
Article in Proceedings |
| Author: |
Glauber Cabral, Christian Maeder, Till Mossakowski, Lutz Schröder |
| Editor: |
Jonathan Aldrich, Ricardo Massa |
| Title: |
Creating a HasCASL library |
| Book / Collection title: |
14th Brazilian Symposium on Programming Languages (SBLP 2010) |
| Year published: |
2010 |
| Abstract: |
A prerequisite for the practical use of a specification language is the
existence of a set of predefined specifications. Although the Common Algebraic
Specification Language (CASL) has a library with such predefined specifications,
its higher order extension, named HASCASL, still lacks a library with
basic higher order data types and functions. In this paper, we describe the specification
and verification of a library for the HASCASL language. Our library
covers a subset of the Haskell Prelude library, including data types and classes
representing Booleans, lists, characters, strings, equality, and ordering functions.
We use the Heterogeneous Tool Set (HETS) for parsing specifications,
generating proof obligations, and translating between the HASCASL and HOL
languages. To discharge the arising proof obligations, we use the Isabelle/HOL
interactive theorem prover. |
| Status: |
Reviewed |
| Last updated: |
16. 05. 2011 |
|
 |
