TY - GEN
T1 - Proof Support for RAISE by a Reuse Approach based on Institutions
AU - Lindegaard, Morten Peter
AU - Haxthausen, Anne Elisabeth
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-540-27815-3_26
DO - 10.1007/978-3-540-27815-3_26
M3 - Article in proceedings
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 319
EP - 333
BT - Proceedings of AMAST'04
PB - Springer Verlag
ER -