The Coq mailing list

[Dale Miller <dale AT cse.psu.edu>]

> 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.

One can change this question to be rather: Should I move my formal
projects (like provers) to a language where unification is supported
declaratively and directly?  The most obvious candidate would be
Prolog, but it is a rather old-fashion language by now and does not
support a lot of modern programming concerns (types, modules,
higher-order programming abstractions, etc) and does not treat syntax
very well itself (lacks occur-check, for example).

There is a much more modern update to Prolog called lambda Prolog.  It
has polymorphic types, modules, abstract datatypes, and higher-order
programming all as part of its declarative core.  It also has a
built-in, logically motivated treatment of syntax containing bound
variables, for which alpha-conversion, correct substitution, sound
unification, etc are primitives.  One domain that this language has
shown promise has been the construction of provers.  For more on this
language, see http://www.cse.psu.edu/~dale/lProlog/.

There is also a new compiler for lambda Prolog called Teyjus, written
by Gopalan Nadathur (http://www.cs.uchicago.edu/~gopalan/).  It
incorporates a lot of new technology described in the recent research
literature that was designed for formal systems: explicit
substitution, lazy substitution, and higher-order patterns (even
higher-order unification).  For more on this implementation, see
http://teyjus.cs.uchicago.edu/.

Coming back to your questions more specifically about extension to
functional programming to support formal system development: the paper
below was an attempt to extended ML with support for bound variables
within syntax.  (It still relies on matching, not unification.)

  "An Extension to ML to Handle Bound Variables in Data
  Structures", by Dale Miller.  Proceedings of the Logical Frameworks
  BRA Workshop, May 1990.
  ftp://ftp.cse.psu.edu/pub/dale/mll.dvi
  ftp://ftp.cse.psu.edu/pub/dale/mll.ps
  ftp://ftp.cse.psu.edu/pub/dale/mll.pdf


 -Dale Miller

Department of Computer Science and Engineering  FAX: 814-865-3176
The Pennsylvania State University               Email: 
dale AT cse.psu.edu
220 Pond Laboratory                             Main Office: 814-865-9505
University Park, PA 16802-6106  USA             http://www.cse.psu.edu/~dale