coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Suppose caml or ML had unification ....

From: Steve Stevenson <steve AT cs.clemson.edu>
To: coq-club AT pauillac.inria.fr, info-hol AT jaguar.cs.byu.edu, isabelle-users AT cl.cam.ac.uk, lego-club AT dcs.ed.ac.uk, nuprllist AT cs.cornell.edu, pvs AT csl.sri.com
Subject: Suppose caml or ML had unification ....
Date: Wed, 1 Sep 1999 08:32:50 -0400 (EDT)

Good morning,

        I'm contemplating extensions to functional languages that
would support development of formal projects like provers. My analysis
says that many implementation issues would go away (or at least be
easier) if functional languages had unification. There was a lot of
work done on this but it doesn't seem to be in the available
compilers.

        Would you please comment on:

        1. Do you agree with the "unification" stance?

        2. If so, what would you like to see as support?
Syntactically? Semantically?

        3. Regarless, what other difficult implementation problems
could be made to go away if the compiler directly support certain
features? Semantics?

Best regards,

steve
-----
Steve (really "D. E.") Stevenson           Assoc Prof
Department of Computer Science, Clemson,   (864)656-5880.mabell
Support V&V mailing list:
ivandv AT cs.clemson.edu

Suppose caml or ML had unification ...., Steve Stevenson
- Re: Suppose caml or ML had unification ...., David von Oheimb
  - Re: Suppose caml or ML had unification ...., Dale Miller