Specify in RSL and Prove in Isabelle

Morten Peter Lindegaard

    Research output: Contribution to conferencePosterResearch

    Abstract

    An approach to increasing proof support for the RAISE method is to translate RSL specifications to Isabelle/HOL and use the theorem prover Isabelle. Institutions and institution representations are used as foundations for the translation. To describe the model-theoretic semantics of RSL, the concept of looser semantics is introduced. An institution for a subset of RSL is presented, higher-order logic is considered, and it is outlined how to translate RSL specifications into Isabelle/HOL.
    Original languageEnglish
    Publication date2002
    Publication statusPublished - 2002
    EventComputer Science and Engineering PhD Day May 2002 -
    Duration: 1 Jan 2002 → …

    Conference

    ConferenceComputer Science and Engineering PhD Day May 2002
    Period01/01/2002 → …

    Bibliographical note

    pp. 45-62
    IMM-TR-2002-8

    Keywords

    • proof support
    • RAISE
    • institutions
    • HOL
    • RSL
    • Isabelle

    Cite this

    Lindegaard, M. P. (2002). Specify in RSL and Prove in Isabelle. Poster session presented at Computer Science and Engineering PhD Day May 2002, .
    Lindegaard, Morten Peter. / Specify in RSL and Prove in Isabelle. Poster session presented at Computer Science and Engineering PhD Day May 2002, .
    @conference{a39864c14fa74f248874c58a6f3135f3,
    title = "Specify in RSL and Prove in Isabelle",
    abstract = "An approach to increasing proof support for the RAISE method is to translate RSL specifications to Isabelle/HOL and use the theorem prover Isabelle. Institutions and institution representations are used as foundations for the translation. To describe the model-theoretic semantics of RSL, the concept of looser semantics is introduced. An institution for a subset of RSL is presented, higher-order logic is considered, and it is outlined how to translate RSL specifications into Isabelle/HOL.",
    keywords = "proof support, RAISE, institutions, HOL, RSL, Isabelle",
    author = "Lindegaard, {Morten Peter}",
    note = "pp. 45-62 IMM-TR-2002-8; Computer Science and Engineering PhD Day May 2002 ; Conference date: 01-01-2002",
    year = "2002",
    language = "English",

    }

    Lindegaard, MP 2002, 'Specify in RSL and Prove in Isabelle' Computer Science and Engineering PhD Day May 2002, 01/01/2002, .

    Specify in RSL and Prove in Isabelle. / Lindegaard, Morten Peter.

    2002. Poster session presented at Computer Science and Engineering PhD Day May 2002, .

    Research output: Contribution to conferencePosterResearch

    TY - CONF

    T1 - Specify in RSL and Prove in Isabelle

    AU - Lindegaard, Morten Peter

    N1 - pp. 45-62 IMM-TR-2002-8

    PY - 2002

    Y1 - 2002

    N2 - An approach to increasing proof support for the RAISE method is to translate RSL specifications to Isabelle/HOL and use the theorem prover Isabelle. Institutions and institution representations are used as foundations for the translation. To describe the model-theoretic semantics of RSL, the concept of looser semantics is introduced. An institution for a subset of RSL is presented, higher-order logic is considered, and it is outlined how to translate RSL specifications into Isabelle/HOL.

    AB - An approach to increasing proof support for the RAISE method is to translate RSL specifications to Isabelle/HOL and use the theorem prover Isabelle. Institutions and institution representations are used as foundations for the translation. To describe the model-theoretic semantics of RSL, the concept of looser semantics is introduced. An institution for a subset of RSL is presented, higher-order logic is considered, and it is outlined how to translate RSL specifications into Isabelle/HOL.

    KW - proof support

    KW - RAISE

    KW - institutions

    KW - HOL

    KW - RSL

    KW - Isabelle

    M3 - Poster

    ER -

    Lindegaard MP. Specify in RSL and Prove in Isabelle. 2002. Poster session presented at Computer Science and Engineering PhD Day May 2002, .