Re: Programming language specification languages

neelk@alum.mit.edu (Neelakantan Krishnaswami)
10 Oct 2001 15:49:14 -0400

          From comp.compilers

Related articles
[3 earlier articles]
Re: Programming language specification languages rkrayhawk@aol.com (2001-09-25)
Re: Programming language specification languages idbaxter@semdesigns.com (Ira D. Baxter) (2001-09-26)
Re: Programming language specification languages vbdis@aol.com (2001-09-26)
Re: Programming language specification languages wclodius@aol.com (2001-10-06)
Re: Programming language specification languages joachim_d@gmx.de (Joachim Durchholz) (2001-10-06)
Re: Programming language specification languages joachim_d@gmx.de (Joachim Durchholz) (2001-10-06)
Re: Programming language specification languages neelk@alum.mit.edu (2001-10-10)
Re: Programming language specification languages wclodius@aol.com (2001-10-20)
Re: Programming language specification languages nmm1@cus.cam.ac.uk (2001-10-21)
| List of all articles for this month |

From: neelk@alum.mit.edu (Neelakantan Krishnaswami)
Newsgroups: comp.compilers
Date: 10 Oct 2001 15:49:14 -0400
Organization: Compilers Central
References: 01-09-087 01-10-020
Keywords: design
Posted-Date: 10 Oct 2001 15:49:14 EDT

On 6 Oct 2001 16:35:54 -0400, Joachim Durchholz <joachim_d@gmx.de> wrote:
>Nick Maclaren <nmm1@cus.cam.ac.uk> wrote:
>> What I want is something enough beyond BNF that I can define
>> type-consistency, scoping, aliasing and value-constraint rules. The
>> really fancy stuff can be said in English.
>
> Take a look at two-level grammars (van Wijngaarden). It's a sort of
> "grammars with attributes"; you stuff the types (and scoping
> information etc.) into the attributes.


I think that I'd rather use a structural operational semantics, since
there seems to be a *lot* more literature about specifying languages
with them. One of their really nice properties is that typechecking
and evaluation can be specified using the same formalism, so that if
you want to define more than typechecking it's easy to extend the
definition.


As for manipulating operational semantics (is that the right plural?),
you should probably use a theorem prover, like Coq or Twelf or Lambda
Prolog. They can help ensure that you don't screw up the algebra at
any stage. (I like Twelf, myself. It has very good Emacs integration.)




Neel


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.