Contributions for Isabelle

Software

• isawin
  A prototype GUI for Isabelle. isawin is a functor representing a parameterised user-interface for a (still prototypical) grafical user-interface for Isabelle. It is based on sml_tk. Sources.

  yats

  A prototypical transformation system based on proven correct transformations like "GlobalSearch"(D. Smith). It is an instantiation of isawin. Sources .

• Kolyang, T.Santen, B. Wolff:
  Correct and User-Friendly Implementations of Transformation Systems. Transformational development systems like PROSPECTRA and KIDS represent an exciting method of program construction. However, the implementation of these systems have traditionally been insecure. This paper shows how the ideas pioneered by these systems can be captured inside a secure LCF style theorem prover like Isabelle. The system yats is a prototypical implementation of this. LNCS 1501.

• Kolyang, T.Santen, B. Wolff:
  A Structure Preserving Encoding of Z. The paper presents a semantic representation of the core concepts of the specification language Z in higher order logic. Although a "shallow embedding", it preserves the structure of the Z specification and avoids expanding Z schemas. The representation conforms with the latest draft of the Z standard. LNCS 1125, 1996

• Embedding of Z in Isabelle/HOL.
  A Shallow Embbeding of Z in Isabelle/HOL.