[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.