Home

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.

By Ehud Lamm at 2005-10-17 13:07 | Theory | other blogs | 9856 reads

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?

By daryabeygi at Mon, 2005-10-17 22:06 | login or register to post comments

Twelf

Twelf is here.

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

By Ehud Lamm at Tue, 2005-10-18 07:38 | login or register to post comments

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?

By daryabeygi at Tue, 2005-10-18 21:25 | login or register to post comments

Semantics, types

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

By Ehud Lamm at Wed, 2005-10-19 08:37 | login or register to post comments

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).

By Carl Witty at Tue, 2005-10-18 00:01 | login or register to post comments

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...

By michaelw at Tue, 2005-10-18 08:15 | login or register to post comments

Example

Remember this story?

By Ehud Lamm at Tue, 2005-10-18 08:29 | login or register to post comments

Page not found

Was it this one?
Meijer: On The (Non) Value of Programming Language Research

By michaelw at Tue, 2005-10-18 08:39 | login or register to post comments

Yes. Thanks.

Yes. Thanks.

By Ehud Lamm at Tue, 2005-10-18 11:10 | login or register to post comments

Article

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.

By Charles Stewart at Fri, 2008-04-11 13:18 | login or register to post comments