Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl, bjacobs@nl.ruu.math
Subject: DTT->HOL paper available by ftp.
Date: Mon, 14 Dec 92 13:58:56 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.840:14.11.92.13.59.25"@cl.cam.ac.uk>


Bart Jacobs and I have been working on a translation of Dependent Type
Theory into the HOL logic.  The expressive power of Dependent Type
Theory (DTT) has several well-known advantages for applications of
formal methods (e.g. see Keith Hanna's recent work). The classical
Higher Order Logic supported by the HOL theorem prover is rather
simpler to use than DTT but less expressive.  The aim of this work has
been to gain the pragmatic advantages of DTT within the simpler HOL
framework by means of a translation of DTT into higher order logic.

I have made a paper on this work available by ftp from ftp.cl.cam.ac.uk 
in the directory /hvg/papers. The relevant file is called DTTinHOL.ps.Z.

The details are:

    Translating Dependent Type Theory into Higher Order Logic

    Bart Jacobs and Tom Melham

    To appear in the proceedings of the International Conference 
    on Typed Lambda Calculi and Applications, Utrecht, 16--18
    March 1993, (Springer-Verlag, LNCS series).

    This paper describes a translation of the complex calculus of
    dependent type theory into the relatively simpler higher order
    logic originally introduced by Church.  In particular, it shows how
    type dependency as found in Martin-Lof's Intuitionistic Type Theory
    can be simulated in the formulation of higher order logic
    mechanized by the HOL theorem-proving system.  The outcome is a
    theorem prover for dependent type theory, built on top of HOL, that
    allows natural and flexible use of set-theoretic notions.  A bit
    more technically, the language of the resulting theorem-prover is
    the internal language of a (boolean) topos (as formulated by Phoa).

Anyone particularly interested in the implementation is welcome
to contact me (tfm@cl.cam.ac.uk).  Please note the final two
sentences of the paper

    "To make the system practical, a very considerable infrastructure
     will have to be built on top of this basis---this still remains
     to be done.  Future work will also involve an investigation of
     how best to mix reasoning in both DTT and HOL."

If anyone wants to consider further development of, or experiments 
with, the implementation---just let me know.

Tom