Re: Programming language specification languages

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

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