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

An attempt to draw a picture of what various meanings of HOL may be, was already made in a prior thread in this news‑group (last year, I believe), and it's indeed rather large, especially for a non‑student/non‑professional.

What I understand from the second paper, is that the “λ” in “λHOL” denotes a reference to the location of the named theory on the lambada‑cube (something I already heard about before).

I had this question wondering if it's something new I did not knew or a new name for something I already knew. To tell more, my guess is: HOL is a friendly name, and λHOL is a more formal name with a reference to the lambda‑cube, so not a new logic (if I'm not wrong).

With thanks for your concern

On Tue, 30 Sep 2014 09:17:21 +0200, Ramana Kumar <rk436 at> 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.

On Tue, Sep 30, 2014 at 4:38 AM, Yannick Duchêne (Hibou57) <yannick_duchene at> wrote:
I guess I found an answer here, , and the >>answer is yes.

Le Mon, 29 Sep 2014 05:51:53 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at> a écrit:

Hi all,

I'm not playing with Isabelle since some time, but still read from time to time on things around it: type theory and >>>proof theory and HOL. I came to a question related to HOL and type theory, and though this may be the best place to ask >>>for, due to Isabelle being very close to it.

I landed onto this paper:

In the abstract, it says “HOL, or its type theoretic variant λHOL”. Does that mean the real name of HOL with simple >>>type theory is λHOL? And also, does that mean there exist(ed) an HOL outside any type theory? (for the latter, I don't >>>see how, but may be I'm too much biased on this). Or I am misunderstanding this sentence?

With thanks, and have a nice day.

--“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Yannick Duchêne

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