[isabelle] Vocabulary question: is the real name of HOL, λHOL?
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