Email Gateway (Aug 18 2022 at 17:01): Email Gateway (Aug 18 2022 at 17:01):From: mark@proof-technologies.com
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.
Mark.
on 17/1/11 10:45 PM, mark@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
to
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@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
Last updated: Nov 21 2024 at 12:39 UTC