Home » forums » LtU Forum

On Presenting Operational Semantics

So as I understand it, describing a language semantics in terms of execution by the SECD machine, is an acceptable presentation of small-step operational semantics. What I don't know is whether small-step operation semantics are still in fashion or considered outdated. One of the practical advantages of small-step operational semantics presented in this manner, seems to me at least, that it facilitates the verification of the language semantics, and for other people to create their own implementations. Is this the common wisdom?

Well given that, I have to wonder why not describe the small-step operational semantics using an even simpler stack machine, one without registers or environment (instead allowing first-class functions on the stack). That seems to me to offer some advantages over the SECD machine. For example, we obviously don't have to worry about environment and registers, and we also don't need to perform defunctionalization.

I am asking, because I want to formally present the semantics (without regard for types) of a simple imperative OO language with some functional features.

Some of my reading material concerning operational semantics:

Please feel free to add more to my list.

By cdiggins at 2008-04-24 16:32 | LtU Forum | previous forum topic | next forum topic | other blogs | 6210 reads

Comment viewing options

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

Felleisen, Hieb & PLT Redex

I'd suggest taking a look at the Felleisen & Hieb approach, which is used by the PLT Redex tool for modeling operational semantics.

There's some background and motivation for this approach, with references, on the page Why PLT Redex?

By Anton van Straaten at Thu, 2008-04-24 17:12 | login or register to post comments

Addition and comments

I would add Formal Semantics of Programming Languages to the list.

cdiggins: One of the practical advantages of small-step operational semantics presented in this manner, seems to me at least, that it facilitates the verification of the language semantics...

Kind of. The standard approach here is natural deduction on inductive definitions based on the abstract syntax of the language, so even just proving type safety, i.e. progress and preservation, tends to be rather tedious—so much so that it's one reason among several why you don't see many certified compilers for languages defined by a small-step operational semantics around—and proving full semantic preservation is... well... not done. It's perhaps worth pointing out that Xavier Leroy's CompCert project uses big-step operational semantics, tackling the dual challenges of distinguishing between partiality and "going wrong" in that setting and representing that setting in the Coq proof assistant; while Adam Chlipala's certified type-preserving compiler for the simply-typed lambda calculus relies on denotational semantics in order to take maximal advantage of Coq's Calculus of Inductive Constructions and support for proof automation.

Having said all of that, most of the popular papers and texts, including the highly-regarded "Types and Programming Languages," continue to present small-step operational semantics; the Coq tutorial at POPL 2008 introduced the U. Penn PL team's tools for mechanized metatheory based on induction over abstract syntax (again, a process at the heart of small-step operational semantics), etc.

In my opinion, the jury is still out over what the best approach to mechanizing metatheory is. I'm putting my chips down on Chlipala's Lambda Tamer approach. But you didn't ask about mechanizing metatheory; you asked about presentation, apparently with an eye toward implementation. From that point of view, I think both your simple stack machine idea and PLT Redex have a lot to recommend themselves for reasons of ease of implementation and visualization.

By Paul Snively at Thu, 2008-04-24 17:46 | login or register to post comments

Thanks

Thank you Paul and Anton for these pointers! This is exactly the kind of thing I was hoping for.

By cdiggins at Thu, 2008-04-24 18:53 | login or register to post comments

Concurrency

One main advantage of small step semantics is that it is much more straightforward for describing concurrent computation models.

By Andreas Rossberg at Thu, 2008-04-24 19:50 | login or register to post comments

ASMs

ASMs have been used to provide semantics for many languages such as C and many others on the asm site. See the complete list with many papers.

By Hank Thediek at Thu, 2008-04-24 21:25 | login or register to post comments

Very helpful, thank you.

Very helpful, thank you. Several of these papers are somewhat old, so I wonder what the modern consensus regarding using ASMs to present language semantics is? What are the advantages and disadvantages?

By cdiggins at Fri, 2008-04-25 14:50 | login or register to post comments

The method goes back a long

The method goes back a long way but is still a going concern. There is a group st Microsoft lead by Yuri Gurevich the originator of the idea. Microsoft supports an executable ASM language called AsmL and some tools shown on the same page.

As far as consensus is concerned I would like to know more myself.

By Hank Thediek at Fri, 2008-04-25 15:55 | login or register to post comments

Andrew Pitts' work on OpSem...

...is really powerful stuff. The idea is not simply to give a formal description of the language, but to use algebraic ideas to present the OpSem in a way that it can be used in a manner similar to denotational semantics for reasoning about programs.

By Charles Stewart at Fri, 2008-04-25 21:57 | login or register to post comments