Proof Support for RAISE by a Reuse Approach based on Institutions

Morten Peter Lindegaard, Anne Elisabeth Haxthausen

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    This paper explains how proof support for the RAISE Specification Language (RSL) can be obtained by reusing the Isabelle/HOL theorem prover. An institution for a subset of RSL is defined together with a light institution comorphism from this institution to an existing institution for higher-order logic (HOL). A translation of RSL specifications to Isabelle/HOL theories is derived from the light institution comorphism and proved sound wrt. semantic entailment. Finally, the results of some case studies are reported. Keywords: Institutions, RSL, HOL, algebraic semantics, proof support.
    Original languageEnglish
    Title of host publicationProceedings of AMAST'04
    PublisherSpringer Verlag
    Publication date2004
    Pages319-333
    DOIs
    Publication statusPublished - 2004
    SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    ISSN0302-9743

    Fingerprint

    Dive into the research topics of 'Proof Support for RAISE by a Reuse Approach based on Institutions'. Together they form a unique fingerprint.

    Cite this