Lambda the Ultimate

inactiveTopic The essence of compiling exceptions
started 2/18/2003; 12:59:42 PM - last post 2/19/2003; 5:00:14 AM
Ehud Lamm - The essence of compiling exceptions  blueArrow
2/18/2003; 12:59:42 PM (reads: 1603, responses: 1)
The essence of compiling exceptions
The essence of compiling exceptions. Graham Hutton and Joel Wright. To be submitted for publication, 2003.

Given the importance of exceptions, it is perhaps surpris­ing that in textbooks and research articles on compilation, exceptions are often not considered at all, or one finds rather brief mention of concepts such as "marking the stack" and "unwinding the stack". In this article we make such ideas precise, by presenting a compiler for a small language with exceptions, together with a proof of its correctness with re­spect to a formal semantics for the language. To the best of our knowledge, this is the first time that a compiler for exceptions has been proved to be correct, but we would welcome any pointers to other work in this area.

A nice, and rather short, paper.

The first two sections (sections 2 and 3), which show a basic compiler for arithmetic expressions and prove its correctness, are well worth reading for their elegance, even if you are not interested in the discussion of compiling exceptions.

It should be noted that the exception mechanism discussed is less expressive than what you would find in languages such as Ada or C++, and the implementation discussed is a bit naive.

EOPL2 devotes section 7.4 to exceptions, but these are implemented using continutations, in the context of a CPS interpreter, so efficient compilation of exceptions isn't covered.

The paper uses Haskell as an executable notation. Interestingly, the authors mention they used QuickCheck while developing the code in the paper and before proving it is correct.

Posted to implementation by Ehud Lamm on 2/18/03; 1:09:18 PM

Sander - Re: The essence of compiling exceptions  blueArrow
2/19/2003; 5:00:14 AM (reads: 436, responses: 0)
Very nice paper! Finally a paper that discusses the details of exception handling implementation.

I'm still trying to find a way to improve the Haskell exception mechanism, so this is an interresting read for me, thanks!