Paper Info
Title
An Embedding of Ruby in Isabelle
Abstract
. This paper describes a semantical embedding of the relationbased language Ruby in Zermelo-Fraenkel set theory (ZF) using theIsabelle theorem prover. A small subset of Ruby, called Pure Ruby, isembedded as a conservative extension of ZF and many useful structuresused in connection with VLSI design are defined in terms of Pure Ruby.The inductive package of Isabelle is used to characterise the Pure Rubysubset to allow proofs to be performed by structural induction over thePure Ruby ...
Year
DOI
Venue
1996
10.1007/3-540-61511-3_80
CADE
Keywords
Field
DocType
set theory,theorem prover,vlsi design
Discrete mathematics,Set theory,Embedding,Computer science,Automated theorem proving,Type rule,Algorithm,Mathematical proof,Conservative extension,Very-large-scale integration,Structural induction
Conference
ISBN
Citations 
PageRank 
3-540-61511-3
2
0.47
References 
Authors
8
1
Name
Order
Citations
PageRank
Ole Rasmussen1274.49