Home » forums » LtU Forum

Specifying semantics and type rules

There are relatively few language specifications out there which incorporate a formal statement of semantics and typing rules. Of those that do, the one that I'm most familiar with (ML) uses a fairly hard to read notation.

We're at the point where we want to incorporate such a statement into the BitC specification, and I'ld appreciate pointers, inputs, and suggestions on how we might express these things with the greatest clarity and precision. It seems to me, naively, that we need to specify how the full language syntax maps (syntactically) to a canonicalized core syntax, and then specify the semantics and typing rules for that core. At the moment, I'm attracted to the notation used by Pierce's book (and of course by others). I'm willing to sacrifice textual compactness for clarity. On the other hand, the idea of formalizing directly in Coq has its appeal.

Are there examples of specifications out there that we should look at as potential exemplars? If so, why are they exemplars? What makes them good. Conversely, are there examples out there of approaches to avoid, and why?

Aside: this isn't the right forum for an extended discussion of formalizing BitC in particular, but if you would like to participate in that process, please do come join the appropriate mailing list.

By shap at 2009-01-22 14:07 | LtU Forum | previous forum topic | next forum topic | other blogs | 5052 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Standard ML

I think the Definition of Standard ML is still a great example and resource for formalizing a practical language. There's a Commentary on the Definition that may also be helpful.

It's been some time since I've looked at the Definition, so I'm curious what part of the notation you find distasteful? I don't seem to remember anything particularly out of the ordinary.

Anyway, I think your general outline is still the usual approach. Desugaring into a canonical core syntax has many advantages in addition to formalization, so it's certainly not a bad first step.

By Matt Hellige at Thu, 2009-01-22 16:35 | login or register to post comments

SML Definition and Commentary

Both are available online, though they moved since the last time they were mentioned on LtU.

By Chris Rathman at Thu, 2009-01-22 17:40 | login or register to post comments

Concerning the ML definition

"Distasteful" was certainly not what I intended to say at all, so in response to your question, I went back and re-examined the ML definition. The last time I tried to process it, I wasn't nearly so far along in my understanding of formalizing semantics and types and so forth. Not that I'm any sort of expert now, but I'm modestly less ignorant.

Looking at it now, I conclude that my main problem with it may have had more to do with the limitations imposed by its typography than anything else. Reading it now, I find that while I have to refer backwards on a couple of things, it mostly makes sense to me.

So thanks for your question! I appreciated the opportunity to re-examine that work.

By shap at Fri, 2009-01-23 13:25 | login or register to post comments

Denotational

First, please, please, please make the semantics denotational. This will greatly ease their formalization down the line.

This is, of course, assuming that you only do the formalization down the line. My next question is: what's stopping you from formalizing BitC using Lambda Tamer?

By Paul Snively at Thu, 2009-01-22 16:42 | login or register to post comments

Denotational semantics

First, please, please, please make the semantics denotational. This will greatly ease their formalization down the line.

What kind of formalization do you mean? If you mean in a theorem prover like Coq or Twelf then it is exactly the opposite.

By Andreas Rossberg at Thu, 2009-01-22 17:02 | login or register to post comments

Denotational vs. Operational Semantics

Sorry, I should have been more clear. Essentially, I subscribe to Adam Chlipala's point of view, which (as best I understand it) is that denotational semantics implemented in terms of, e.g. Coq prevent one from having to develop a lot of progress and preservation proofs (see slide 21), and using the Calculus of Inductive Constructions as the metalanguage buys you a lot of your dynamic semantics "for free" (see the "Certified Compilers Now!" section of Adam's home page, item 3). Of course, the counter may very well be that some aspects of a practical programming language, e.g. state, are quite challenging to formalize denotationally, and I'll note this point in advance. :-) The current version of Lambda Tamer does support the use of state, but as far as I know, we're still waiting for documentation on that aspect of the system. Perhaps Adam can shed more light on this.

By Paul Snively at Fri, 2009-01-23 03:06 | login or register to post comments

Ott: Tool Support for Semantics

You might have some use for OTT. I haven't used it myself, but the examples (a subset of ocaml, and lightweight java) look promising. You could ask the XQuery and scheme folks what (didn't)work for their specifications.

By Ethan Aubin at Thu, 2009-01-22 17:37 | login or register to post comments