Re: [isabelle] Polymorphism and simple type
On Mon, 17 Jan 2011, Steve W wrote:
I have a question about Isabelle's polymorphism. Since Isabelle has a
simply-typed lambda calculus, how come the meta-logic is polymorphic?
Funny thing (1): Isabelle/Pure is not really a meta-logic, because it
cannot reason much about other logics. This is why I prefer to call it
"logical framework", according to what I've learned from Stefan Berghofer
at some point.
Funny thing (2): Isabelle/Pure is not polymorphic either. You can work
schematically wrt. arbitrary types and the system juggles contexts and
results in a way that it looks like Hindley-Milner polymorphism. See also
the explanation of the "admissible rules generalize and instantiate" in
the Isabelle/Isar implementation manual (chapter 2).
This archive was generated by a fusion of
Pipermail (Mailman edition) and