Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 25 Oct 1993 20:07:35 +0000 Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA20698; Mon, 25 Oct 93 13:56:25 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.4/16.2) id AA20677; Mon, 25 Oct 93 13:56:19 -0600 Received: from panther.cs.uidaho.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA13630; Mon, 25 Oct 93 12:53:26 -0700 Received: by panther.cs.uidaho.edu id AA09466 (5.65c/IDA-1.4.4 for info-hol@cs.uidaho.edu); Mon, 25 Oct 1993 12:52:01 -0700 Date: Mon, 25 Oct 1993 12:52:01 -0700 From: Chris Toshok Message-Id: <199310251952.AA09466@panther.cs.uidaho.edu> To: info-hol@cs.uidaho.edu Subject: Specification languages in HOL Hello all, I was wondering if there had been any work done in HOL with any specification languages (Z for example). I am looking specifically for references or information on verifying code by way of a semantic description and a specification. Any information would be greatly appreciated. Cheers, toshok ==================================================================== Chris Toshok | "To tuple is human, | to curry, divine" toshok@.cs.uidaho.edu | - anonymous functional | programmer ====================================================================