@MISC\{IMM2002-01173,
    author       = "M. P. Lindegaard",
    title        = "Specify in {RSL} and Prove in Isabelle",
    year         = "2002",
    month        = "may",
    keywords     = "{RSL,} Isabelle, {HOL,} {RAISE,} proof support, institutions.",
    pages        = "45-62",
    publisher    = "{IMM,} Technical University of Denmark",
    address      = "{DTU,} {DK-}2800 Kgs. Lyngby",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/1173-full.html",
    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.",
    isbn_issn    = "IMM-TR-2002-8"
}