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