*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Is Isabelle/Pure really a meta-logic?*From*: Steve Wong <s.wong.731 at gmail.com>*Date*: Sat, 25 Aug 2012 13:20:20 +0100*Cc*: John Munroe <munddr at gmail.com>, Randy Pollack <rpollack0 at gmail.com>, Ramana Kumar <rk436 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <23540A27-A5C5-4F00-BE1E-606620D35A59@cam.ac.uk>*References*: <CAP0k5J5bGrsyX4exRntzOF94tm_gJ=M-u_D4Jzbm1C48mfk3MQ@mail.gmail.com> <CAMej=24ERc8Pgpjt+GEmWm4htmDmeLk-fF7JaqQb=3LCOUH-Yg@mail.gmail.com> <CAP0k5J4kru8JDPjdh+NHcKCQiaAHV5g_gd5Ls8nQJhw_yZmT+A@mail.gmail.com> <E90E39CF-B3A4-49D2-AACA-7D4E5A77EB55@cam.ac.uk> <CAP0k5J6nEgz19-kgUX108DfZhpezz-5LDMQas1NyTmAS8FKCDg@mail.gmail.com> <CANofLeJRWT+Nf1Wn+nBSnKnfi4mpUs3bD3udfYsAHaZ4UeVfxA@mail.gmail.com> <23540A27-A5C5-4F00-BE1E-606620D35A59@cam.ac.uk>

Regarding the remark about higher-order abstract syntax, should one call the Term datatype in Term.ML HOAS? If I understand correctly, Its purpose is to bind the meta-language to the the object-language. Cheers Steve On Wed, Aug 22, 2012 at 7:51 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > Also called a meta-logical-framework. I prefer that name as being more > uniform. > Larry > > On 22 Aug 2012, at 19:07, Randy Pollack <rpollack0 at gmail.com> wrote: > > > A metalogic formalizes the construction of the syntax of the object > > logic, usually as true inductive objects, allowing induction over the > > construction of these objects. > > >

**References**:**[isabelle] Is Isabelle/Pure really a meta-logic?***From:*John Munroe

**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*Ramana Kumar

**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*John Munroe

**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*Lawrence Paulson

**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*John Munroe

**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*Lawrence Paulson

- Previous by Date: [isabelle] Object-reasoning
- Next by Date: Re: [isabelle] Object-reasoning
- Previous by Thread: Re: [isabelle] Is Isabelle/Pure really a meta-logic?
- Next by Thread: [isabelle] Defining {x} == {x, x} using "syntax", "translations", & one function
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list