Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?

On Tue, 3 Mar 2015, Larry Paulson wrote:

I think your clue here is the phrase "type-theoretic parlanceâ, which is to say that people from that background may want to see ==> as a function type, for example, analogously to LF, which can be regarded as the type-theoretic analogue of Isabelle Pure.

Yes, this text in the "isar-ref" manual (section 2.1) and a slightly longer version in the "implementation" manual (chapter 2) emerged from what I've learned from people in Edinburgh, Cambridge, Nijmegen, and especially Stefan Berghofer in Munich around 2000. It is an attempt to explain things in a way that everybody understands, both strongly-dependent types and classic logicians.

On 3 Mar 2015, at 12:48, Askar Safin <safinaskar at> wrote:

The document is isar-ref from isabelle 2013.

By the default, you should use the current official release for everything, including the continously growing/updated manuals. Presently it is Isabelle2014 (August 2014).

Also, FAQ doesn't say about levels of lambda calculi.

Before Larry mentioned that, I hardly remembered this ancient relic at all. Apart from the isabelle-users mailing list, the current Q&A platform is Stackoverflow:

You should quickly get some idea who is active where, and which kind of discussions or question/answer threads are better place on this site or that site.


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