Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Mon, 31 Aug 92 09:36:34 +0200
From: Lars Rosen <lr@dk.dth.id>
Message-Id: <9208310736.AA04989@idcad7.id.dth.dk>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: sara kalvala's message of Fri, 28 Aug 92 18:12:26 -0700 <9208290112.AA01517@dewdrop.cs.ucdavis.edu>
Subject: Isabelle


>-----
>HOL and Isabelle are based on many of the same principles.  However,
>Isabelle also provides support for unification and embedded logics, and
>therefore could provide a better environment for large proofs than HOL.  We
>propose to investigate whether this really is the case.  We shall evaluate
>Isabelle on major hardware/system verifications.
>-----

>Hopefully we can answer your question in detail later. I would like to
>know if anyone else has already attempted proofs in both and has any
>opinions at present.

>							- Sara


I have been working on proof assistant for the Ruby design calculus.
My first attempt was an embedding in the HOL (pre. 88) prover. This is
documented in:
@techreport(lr:tech,
   author = "Lars Rossen",
   title = "{HOL Formalisation of Ruby}",
   institution= {Dept. of Computer Science Technical University of Denmark},
   number={ID-TR:1989-61},
   year = 1989)
The main conclusion on this work is that the HOL type system is not
sufficiently advanced to express the typing of Ruby (needs term
parameterisation of types).

My next attempt was to implement the Ruby calculus in the Isabelle HOL
logic. This was in a pre. Isabelle 90 (and 92) where the HOL logic
inherited features from CTT. This HOL did enable me to implement a
Ruby proof system, but other problems arose. First; I am not
satisfied with the consistency considerations that I have on this new
logic. Secondly; The type inference became part of the proof
obligation (a consequence of the stronger type system), and this
cluttered up the proofs, it would be nice to be able to separate it
more than my (simple) implementation did. This work is documented in:
@phdthesis(lr:phd,
   author = "Lars Rossen",
   title = "{A relational approach to sequential VLSI design}",
   school= {Dept. of Computer Science Technical University of Denmark},
   year = 1992)

I am not satisfied with any of the implementations, and I believe both
could be improved (especially in the light of new developments on both
HOL and Isabelle). However the work has given me a good working
practice on both provers. Also I feel confident that implementing Ruby
is a good way to exercise a theorem prover as it tests the provers
ability to do generic proofs (typically embedded in the types).

See you at hol92?
               Lars
+-----------------------------------------------------------------------------+
| Lars Rossen                          E-mail: lr@id.dth.dk                   |
| Department of Computer science       Phone : +45 42 88 22 22 ext 3729       |
| Building 344                         Fax   : +45 42 88 22 39                |
| Technical University of Denmark      Home  : Phone: +45 36 70 36 76         |
| DK-2800 Lyngby, Denmark              Knud Anchersvej 95, 2610 R{\o}dovre    |
+-----------------------------------------------------------------------------+
|      **    I wish the Real World was delay insensitive          **          |
+-----------------------------------------------------------------------------+