Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <21086-0@swan.cl.cam.ac.uk>; Thu, 19 Mar 1992 16:22:26 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28631; Thu, 19 Mar 92 07:57:14 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28627; Thu, 19 Mar 92 07:57:05 -0800 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <20642-0@swan.cl.cam.ac.uk>; Thu, 19 Mar 1992 15:59:32 +0000 To: des@uk.co.inmos Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: Ruby in HOL In-Reply-To: Your message of Thu, 19 Mar 92 15:25:41 +0000. <17876.9203191525@frogland.inmos.co.uk> Date: Thu, 19 Mar 92 15:59:29 +0000 From: Tom Melham Message-Id: <"swan.cl.ca.647:19.02.92.15.59.40"@cl.cam.ac.uk> Regarding David Shepherd's question: > did someone once rpesent some work on putting Ruby style hardware > designs manipulation in HOL or am I imagining things. just that i'm > doing something vaguely along those lines at the moment and would > be intereseted in any pointers to existing work. Here are some references: Lars Rossen, `HOL Formalisation of RUBY', Technical Report ID-TR: 1989-61, Department of Computer Science, Technical University of Denmark (November, 1989). Lars Rossen, `Proving (facts about) Ruby', in IV Higher Order Workshop, edited by G. Birtwistle, Workshops in Computing series (Springer-Verlag, 1991), pp 265-283. The email address for Lars Rossen is lr@id.dth.dk Tom