Mechanizing Language Definitions

The problem: Most languages don't have formal specifications.

The solution (maybe): Make specification easier by using mechanized tools (for example, use Twelf).

The presentation: here (Robert Harper, ICFP'05).

The conclusion: You decide.

Comment viewing options

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

in need of direction

this looks very interesting. however, I don't understand any of it. Can someone point me in the general direction of the road to understanding the notations used in this article?


Twelf is here.

If you ask more specific questions, we can try to help.

Thanks, I started to look int

Thanks, I started to look into the twelf documentation. But am I mistaken that the characters in green are not twelf?

Semantics, types

It would seem that green is for the language semantics. TAPL is your friend.

this is the POPLmark Challenge

Note that (as the slides briefly mention) the authors are working on a solution to the POPLmark Challenge (which was mentioned on LtU here).

Grunt work

Recently, we formalized a quite dated but still used language (via SOS rules and translation procedure, and we even completed a faithful implementation of our semantics), and our experience was that it was not appreciated much. Comments were along the lines of "but what is it good for? I doubt the spec is useful, we already had one [in prose], and a [single] implementation...".

Well, we needed the spec for our own purposes anyway. It is not very surprising that we had to do quite some experimentation to find out what certain language elements were really supposed to do.

Ironically, said language is from the Formal Methods field...


Remember this story?

Page not found

Yes. Thanks.

Yes. Thanks.


Harper & Licata wrote up these ideas into a paper that they submitted to the Journal of Functional programming last year. The preprint is available from RH's website.