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

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:
``http://www.cs.ru.nl/~herman/PUBS/inconsist-hol.pdf
`

`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

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