Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?



On Tue, 30 Sep 2014, Ramana Kumar wrote:

You might want confirmation from more than one author on this, or at least
someone who isn't primarily using dependently typed systems. Certainly I
find the sentence you quoted from the abstract of the first paper
confusing. But there are many variations on what is called "HOL"; it would
be nice to find a paper that does a comprehensive summary and comparison.

An important alternative view of "H.O.L." is the paper by William Farmer:

  The Seven Virtues of Simple Type Theory
  imps.mcmaster.ca/doc/seven-virtues.pdf

"Simple Type Theory" is the original name of the game, before it was rephrased by Mike Gordon with the addition of naive polymorphism, and the well-known type definitions that are not really definitional. In Isabelle/HOL there are further re-interpretations with type classes and overloaded definitions.

It would be great, if we could eventually all agree on just one fully formalized understanding of what "HOL" really is. The CakeML and/or OpenTheory projects could be a starting point for this.


	Makarius


----------------------------------------------------------------------------
                   http://stop-ttip.org  738,791 people so far
----------------------------------------------------------------------------




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.