[isabelle] HOL Glossary

By the way, I've written an extensive glossary of HOL-related terminology.
Please feel free to download it from my website:


It has 218 entries, explaining various concepts of formal logic, theorem
prover architecture, ML and HOL, for the purposes of understanding the HOL
logic and how LCF-style theorem provers work.  It is written for HOL Zero
but is largely relevant for all HOL systems.

Any criticisms are gratefully received.


on 17/1/11 10:45 PM, mark at proof-technologies.com wrote:

> Actually the term "simply-typed" tends to be used in more than one way.
> Some people use it to mean "not dependently-typed" and some people use it
> mean "not polymorphic and not dependently-typed".
> When people refer to "simply-typed lambda calculus" they are (usually)
> referring to Church's original simply typed lambda calculus (which he
> created after his untyped lambda calculus).  This does not have
> polymorphism, but Isabelle and HOL, that are based on it, do.
> Mark.
> on 17/1/11 6:01 PM, Steve W <s.wong.731 at gmail.com> wrote:
>> Hi,
>> I have a question about Isabelle's polymorphism. Since Isabelle has a
>> simply-typed lambda calculus, how come the meta-logic is polymorphic?
>> Polymorphism is not typically considered simple, right?
>> Regards
>> Steve

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