Specify in RSL and Prove in Isabelle

Morten Peter Lindegaard

Specify in RSL and Prove in Isabelle

Morten Peter Lindegaard

Research output: Contribution to conference › Poster › Research

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 language	English
Publication date	2002
Publication status	Published - 2002
Event	Computer Science and Engineering PhD Day May 2002 - Duration: 1 Jan 2002 → …

Conference

Conference	Computer Science and Engineering PhD Day May 2002
Period	01/01/2002 → …

Bibliographical note

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

Keywords

proof support
RAISE
institutions
HOL
RSL
Isabelle

OpenUrl availability

Full text

Cite this

@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",

}

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

T2 - Computer Science and Engineering PhD Day May 2002

Y2 - 1 January 2002

ER -

Specify in RSL and Prove in Isabelle

Abstract

Conference

Bibliographical note

Keywords

OpenUrl availability

Fingerprint

Cite this