archives

Formal Compiler Implementation in a Logical Framework

Hickey, Jason and Nogin, Aleksey and Granicz, Adam and Aydemir, Brian (2003) Formal Compiler Implementation in a Logical Framework. Technical Report. California Institute of Technology.

The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of rewrite rules that are written in the language of formal mathematics. In addition, the logical framework guarantees the preservation of scoping, and it automates many frequently-occurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a general-purpose language like ML, in part because of automation, and also because the framework provides extensive support for examination, validation, and debugging of the compiler transformations. The paper is organized around a case study, using the MetaPRL logical framework to compile an ML-like language to Intel x86 assembly. We also present a scoped formalization of x86 assembly in which all registers are immutable.

I don't understand the details of this paper, but the general approach of using rewriting for compilation (including passes such as closure conversion) is very interesting in itself.

(Edit: As a bonus, the paper is derived from the literate MetaPRL sources.)

(Edit: Oleg's applicative-order term rewriting system for code generation shows how simpler rewriting systems can be used in the context of compilation.)

Racket Released

Racket is a programming language. Racket is the language implementation formerly known as PLT Scheme. Racket is available now. To quote the release announcement:

With Racket, you can script command shells and web servers; you can
quickly prototype animations and complex GUIs; regexps and threads
are here to serve you. To organize your systems, you can mix and
match classes, modules or components. Best of all, you start
without writing down types. If you later wish to turn your script
into a program, equip your Racket modules with explicit type
declarations as you wish. And Racket doesn't just come as a typed
variant; you can also write your modules in a purely functional and
lazy dialect.

Racket comes in so many flavors because Racket is much more than a
standard scripting language or a plain programming language. Racket
supports language extensibility to an unequaled degree. A Racket
programmer knows that making up a new language is as easy as writing
a new library.

If you haven't looked at, say, Typed Racket or how to create your own languages in Racket, now might be a good time.

Rosetta Challenge Tasks added to the 2010 Dyalog Programming Contest

In response to feedback suggesting that the suite of tasks in the 2010
Dyalog Programming Contest appears to be a little more comprehensive
than many students have time for at this busy part of the academic
year, we have decided to add a 'Rosetta Code Challenge' to the 2010
Programming Contest, which will run in parallel with the main
programming competition. Six weeks remain until the submission
deadline on July 18th.

Rosettacode.org is a site which presents solutions to the same (nearly
400) tasks in as many different programming languages as possible. At
this time, a relatively small number of solutions have been posted in
APL, so we are keen to encourage APL users to submit more APL
solutions. To this end, we are offering a USD 250 prize for the best
solution to each of the following five (fun!) problems selected from
rosettacode.org:

1. Animate a pendulum
2. Knapsack problem
3. Happy numbers
4. Hofstadter-Conway sequence
5. Monty Hall problem

See the Rosetta Code Challenge page at http://www.dyalog.com/contest_2010/rosetta_challenge.html
for more details on how to participate. The terms and conditions of
the main programming competition are not affected by the Rosetta Code
Challenge, with the exception that anyone who submits solutions for
two or more tasks in EITHER competition will participate in the
drawing for the 20 consolation prizes worth USD 100 each.

As is the case for the main Dyalog Programming Contest, you can win
the same amount of prize money by referring a winner to the
competition as you can by actually participating. While prize winners
must be eligible for an Educational License for Dyalog APL, anyone can
win referral awards! Be the person who refers the winners for all five
Rosetta Challenge tasks and you could win USD 1,250!

Best Regards,

Morten Kromberg
CTO, Dyalog Ltd

SIGPLAN's first Programming Languages Software Award goes to LLVM

ACM Press Release:

The ACM Special Interest Group on Programming Languages (SIGPLAN) today presents its first-ever Programming Languages Software Award to Chris Lattner of Apple Inc. for his design and development of the Low Level Virtual Machine (LLVM), a compiler infrastructure that has been quickly adopted by a wide array of industry and academic organizations. Since LLVM’s release as an open source compiler infrastructure in October 2003, companies including Apple, Adobe, and Cray have incorporated it into their commercial products, reflecting its simplicity, flexibility, and versatility.