An embedding of ruby in isabelle

Abstract

This paper describes a semantical embedding of the relation based language Ruby in Zermelo-Fraenkel set theory (ZF) using the Isabelle theorem prover. A small subset of Ruby, called Pure Ruby, is embedded as a conservative extension of ZF and many useful structures used in connection with VLSI design are defined in terms of Pure Ruby. The inductive package of Isabelle is used to characterise the Pure Ruby subset to allow proofs to be performed by structural induction over the Pure Ruby elements.