[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.
> on 17/1/11 6:01 PM, Steve W <s.wong.731 at gmail.com> wrote:
>> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and