Lambda the Ultimate

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

Tropical Semirings, Jean-Éric Pin. Idempotency 1994.

It is a well-known fact that the boolean calculus is one of the mathematical foundations of electronic computers. This explains the important role of the boolean semiring in computer science. The aim of this paper is to present other semirings that occur in theoretical computer science. These semirings were baptized tropical semirings by Dominique Perrin in honour of the pioneering work of our brazilian colleague and friend Imre Simon, but are also commonly known as (min, +)-semirings.

In the previous post, Ohad Kammar asked for some more examples of why we should care about adjunctions, which reminded me of one of my favorite examples. You can understand solving many optimization problems as looking for a Galois connection between your problem and the tropical semiring. (Galois connections in general are one of the sources of the program derivation superpowers of the Squiggolists. So if you want to prove programs like Shin Cheng-Mu does, it's worth understanding!)

explains Lawvere’s remark about ‘the familiar Galois connection between sets of axioms and classes of models, for a fixed [signature]‘

Seems like a rather nice introduction to the notion of Galois connection (I seem to remember someone asking about this awhile back).

One place Galois connections pop up is in the realm of Abstract Interpretation.

Berp is an implementation of Python 3. At its heart is a translator, which takes Python code as input and generates Haskell code as output. The Haskell code is fed into a Haskell compiler (GHC) for compilation to machine code or interpretation as byte code.

This project sounds interesting. Has anyone checked it out?

Milawa: A Self-Verifying Theorem Prover for an ACL2-Like Logic

Milawa is a "self-verifying" theorem prover for an ACL2-like logic.

We begin with a simple proof checker, call it A, which is short enough to verify by the "social process" of mathematics.

We then develop a series of increasingly powerful proof checkers, call them B, C, D, and so on. We show that each of these is sound: they accept only the same formulas as A. We use A to verify B, and B to verify C, and so on. Then, since we trust A, and A says B is sound, we can trust B, and so on for C, D, and the rest.

Our final proof checker is really a theorem prover; it can carry out a goal-directed proof search using assumptions, calculation, rewrite rules, and so on. We use this theorem prover to discover the proofs of soundness for B, C, and so on, and to emit these proofs in a format that A can check. Hence, "self verifying."

This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview.

Peter J. Denning and Jack B. Dennis, The Resurgence of Parallelism, Communications of the ACM, Vol. 53 No. 6, Pages 30-32, 10.1145/1743546.1743560

"Multi-core chips are a new paradigm!" "We are entering the age of parallelism!" These are today's faddish rallying cries for new lines of research and commercial development. ... The parallel architecture research of the 1960s and 1970s solved many problems that are being encountered today. Our objective in this column is to recall the most important of these results and urge their resurrection.

A brief but timely reminder that we should avoid reinventing the wheel. Denning and Dennis give a nice capsule summary of the history of parallel computing research, and highlight some of the key ideas that came out of earlier research on parallel computing. This isn't a technically deep article. But it gives a quick overview of the field, and tries to identify some of the things that actually are research challenges rather than problems for which the solutions have seemingly been forgotten.

Functional Pearl: Species and Functors and Types, Oh My! Brent Yorgey, draft.

We've discussed species many times before, and discussed at least one introduction for functional programmers. Here's another, this time considerably less technical. I would say this paper succeeds fairly well in giving a conceptual overview and some useful intuition. If you found the Carette and Uszkay paper sketchy in places, you may find this a gentler introduction.

On the other hand, I don't really see how it counts as a Functional Pearl...

Vincent Cremet and Philippe Altherr: Adding Type Constructor Parameterization to Java, JOT vol. 7, no. 5.

We present a generalization of Java’s parametric polymorphism that enables parameterization of classes and methods by type constructors, i.e., functions from types to types. Our extension is formalized as a calculus called FGJ_ω. It is implemented in a prototype compiler and its type system is proven safe and decidable. We describe our extension and motivate its introduction in an object-oriented context through two examples: the definition of generic data-types with binary methods and the definition of generalized algebraic data-types. The Coq proof assistant was used to formalize FGJ_ω and to mechanically check its proof of type safety.

FGJ_ω is a simple extension of (Featherweight) Java's generics, where type parameters may be type constructors (functions from types to types). This very readable paper finally made me understand GADTs.

(Previously: Generics of a Higher Kind on Scala's support for the same idea.)

Kim Rose and Ian Piumarta have put together a hardbound, soft cloth, foil stamped book in honor of their friend and colleage, Alan Kay.

See: http://vpri.org/pov/

Click on the blue book for the free PDF version. You can also purchase a traditional copy.

While I like the general idea, it seems this project didn't go far enough.

What I think would be cool is to develop are DSLs that compile to g-code. For example, putting my hacker hat on, I think it might be fun to build a DSL for describing mechanical (analog) computers, this will compile into g-code for cams, shafts, gears etc. that could then be manufactured using CNC machines and/or 3D printers...