Lambda the Ultimate

Verified Just-In-Time Compiler on x86
Magnus O. Myreen

This paper presents a method for creating formally correct just-in-time (JIT) compilers. The tractability of our approach is demonstrated through, what we believe is the first, verification of a JIT compiler with respect to a realistic semantics of self-modifying x86 machine code. Our semantics includes a model of the instruction cache. Two versions of the verified JIT compiler are presented: one generates all of the machine code at once, the other one is incremental i.e. produces code on-demand. All proofs have been performed inside the HOL4 theorem prover.

(To appear in next week's POPL.)

I've been enjoying this paper on my commute this week. It's a nice little distillation of some of the basics of the engineering structure of a JITted language and how the pieces fit together in a correct implementation. As JIT compilers become more and more commonplace, I'd like to see them presented in such a way that they're no more scary or daunting -- at least in principle -- than traditional offline compilers. Perhaps a chapter in EoPL4?

Quantum Lambda Calculus
Peter Selinger, Benoît Valiron

We discuss the design of a typed lambda calculus for quantum computation. After a brief discussion of the role of higher-order functions in quantum information theory, we define the quantum lambda calculus and its operational semantics. Safety invariants, such as the no-cloning property, are enforced by a static type system that is based on intuitionistic linear logic. We also describe a type inference algorithm, and a categorical semantics.

Quantum programming languages have been discussed before on LtU, but there hasn't been a lot of activity lately. I just came across this paper from 2009 that develops the idea of entangled functions.