*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Tue, 30 Sep 2014 05:38:00 +0200*Organization*: Ada @ Home*References*: <op.xmxjoranule2fv@cardamome>*User-agent*: Opera Mail/12.16 (Linux)

Hi all,I'm not playing with Isabelle since some time, but still read from timeto time on things around it: type theory and proof theory and HOL. Icame to a question related to HOL and type theory, and though this maybe 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.pdfIn the abstract, it says “HOL, or its type theoretic variant λHOL”. Doesthat mean the real name of HOL with simple type theory is λHOL? Andalso, 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 onthis). 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

**Follow-Ups**:**Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?***From:*Ramana Kumar

**References**:**[isabelle] Vocabulary question: is the real name of HOL, λHOL?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] rule induction question
- Next by Date: Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?
- Previous by Thread: [isabelle] Vocabulary question: is the real name of HOL, λHOL?
- Next by Thread: Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list