*To*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Tue, 30 Sep 2014 08:17:21 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.xmzdpmm2ule2fv@cardamome>*References*: <op.xmxjoranule2fv@cardamome> <op.xmzdpmm2ule2fv@cardamome>*Sender*: ramana.kumar at gmail.com

You might want confirmation from more than one author on this, or at least someone who isn't primarily using dependently typed systems. Certainly I find the sentence you quoted from the abstract of the first paper confusing. But there are many variations on what is called "HOL"; it would be nice to find a paper that does a comprehensive summary and comparison. On Tue, Sep 30, 2014 at 4:38 AM, Yannick Duchêne (Hibou57) < yannick_duchene at yahoo.fr> wrote: > I guess I found an answer here, http://www.cse.chalmers.se/ > research/group/logic/TypesSS05/Extra/geuvers_sl3.pdf , 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: > > > 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 > > >

**Follow-Ups**:

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

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

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