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


	Makarius





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