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



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



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