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
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 cam.ac.uk> 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
On Tue, Sep 30, 2014 at 4:38 AM, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> 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 yahoo.fr> a écrit:
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and