Lambda the Ultimate

While PHP deservedly gets a terrible rep around programming language folks, this is still an interesting announcement: HipHop compiles PHP down to C++ and gets about a 2x speedup. HipHop will be released as open source, and is currently in production use, serving 90% of Facebook's traffic. It makes me wish Facebook used Python: a large-scale deployment like this would be a great boon to the PyPy project.

Delimited Control in OCaml, Abstractly and Concretely, System Description

We describe the first implementation of multi-prompt delimited control operators in OCaml that is direct in that it captures only the needed part of the control stack. The implementation is a library that requires no changes to the OCaml compiler or run-time, so it is perfectly compatible with existing OCaml source code and byte-code. The library has been in fruitful practical use for four years.

We present the library as an implementation of an abstract machine derived by elaborating the definitional machine. The abstract view lets us distill a minimalistic API, scAPI, sufficient for implementing multi-prompt delimited control. We argue that a language system that supports exception and stack-overflow handling supports scAPI. Our library illustrates how to use scAPI to implement multi-prompt delimited control in a typed language. The approach is general and can be used to add multi-prompt delimited control to other existing language systems.

Oleg was kind enough to send me an e-mail letting me know of this paper's existence (it appears not yet to be linked from the "Computation" page under which it is stored) and to include me in the acknowledgements. Since the paper in its current form has been accepted for publication, he indicated that it can be made more widely available, so here it is. In typical Oleg fashion, it offers insights at both the theoretical and implementation levels.

Leo Meyerovich recently started a thread on LtU asking about Historical or sociological studies of programming language evolution?. I've been meaning to post a paper on this topic to LtU for awhile now, but simply cherrypicking for the opportune time to fit it into forum discussion. With Leo's question at hand, I give you an interesting paper that models language evolution, by artificial intelligence researcher Luc Steels. Steels has spent over 10 years researching this area, and his recent paper, The Recruitment Theory of Language Origins, summarizes one of his models for dealing with language evolution:

The recruitment theory of language origins argues that language users recruit and try out different strategies for solving the task of communication and retain those that maximise communicative success and cognitive economy. Each strategy requires specific cognitive neural mechanisms, which in themselves serve a wide range of purposes and therefore may have evolved or could be learned independently of language. The application of a strategy has an impact on the properties of the emergent language and this fixates the use of the strategy in the population. Although neurological evidence can be used to show that certain cognitive neural mechanisms are common to linguistic and non-linguistic tasks, this only shows that recruitment has happened, not why. To show the latter, we need models demonstrating that the recruitment of a particular strategy and hence the mechanisms to carry out this strategy lead to a better communication system. This paper gives concrete examples how such models can be built and shows the kinds of results that can be expected from them.

I owe Martin Odersky and his team at EPFL an apology: as you can see, I'm posting this rather dramatically late, as the deadline for submission has already passed. Nevertheless, hopefully the notice of the event itself is still worthwhile.

Sheepishly,
Paul

The First Scala Workshop
========================

Call for Papers
---------------

Scala is a general purpose programming language designed to express
common programming patterns in a concise, elegant, and type-safe
way. It smoothly integrates features of object-oriented and
functional languages.

This workshop is a forum for researchers and practitioners to share
new ideas and results of interest to the Scala community. The first
workshop will be held at EPFL in Lausanne, Switzerland, on Thursday
15 April 2010, co-located with Scala Days 2010 (15-16 April).

We seek papers on topics related to Scala, including (but not
limited to):

1. Language design and implementation -- language extensions,
optimization, and performance evaluation.

2. Library design and implementation patterns for extending Scala --
embedded domain-specific languages, combining language features,
generic and meta-programming.

3.Formal techniques for Scala-like programs -- formalizations of the
language, type system, and semantics, formalizing proposed language
extensions and variants, dependent object types, type and effect
systems.

4. Concurrent and distributed programming -- libraries, frameworks,
language extensions, programming paradigms: (Actors, STM, ...),
performance evaluation, experimental results.

5. Safety and reliability -- pluggable type systems, contracts,
static analysis and verification, runtime monitoring.

6. Tools -- development environments, debuggers, refactoring
tools, testing frameworks.

7. Case studies, experience reports, and pearls

Important Dates
---------------

Submission: Friday, Jan 15, 2010 (24:00 in Apia, Samoa)
Notification: Monday, Feb 15, 2010
Final revision: Monday, Mar 15, 2010
Workshop: Thursday, Apr 15, 2010

Submission Guidelines
---------------------

Submitted papers should describe new ideas, experimental results, or
projects related to Scala. In order to encourage lively discussion,
submitted papers may describe work in progress. All papers will be
judged on a combination of correctness, significance, novelty,
clarity, and interest to the community.

Submissions must be in English and at most 12 pages total length in
the standard ACM SIGPLAN two-column conference format (10pt).
No formal proceedings will be published, but there will be a webpage
linking to all accepted papers. The workshop also welcomes short papers.

Submission instructions will be published at:
http://www.scala-lang.org/days2010

Program Committee
-----------------

Ian Clarke, Uprizer Labs
William Cook, UT Austin
Adriaan Moors, KU Leuven
Martin Odersky, EPFL (chair)
Kunle Olukotun, Stanford University
David Pollak, Liftweb
Lex Spoon, Google

Picture or screenshot driven programming from the MIT.

From the Sikuli project page:

Sikuli is a visual technology to search and automate graphical user interfaces (GUI) using images (screenshots). The first release of Sikuli contains Sikuli Script, a visual scripting API for Jython, and Sikuli IDE, an integrated development environment for writing visual scripts with screenshots easily.

Useful presentation.
The most intriguing part, of course, is the Clojure-in-Clojure bit.

I have done some work recently on the theory of aliasing, which I believe provides the key to the frame problem and more generally to proving O-O programs (although these applications remain to be better explained and explored further).

I was struck by the simplicity and generality of the laws uncovered in the process.

A blog entry at bertrandmeyer.com presents the basics. It includes a link to the draft paper, and also to a downloadable version of the implementation (currently a Windows executable, the source will be released later), which makes it possible to test all the examples of the paper.

-- Bertrand Meyer

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?

ScalaModules is an open source project aimed at providing fluent support for OSGi to Scala developers. It takes advantage of Scala's infix operator notation, higher order functions, and implicit conversions. ScalaModules transparently uses the Scala compiler to wrap an OSGi BundleContext with its own RichBundleContext model.

This general technique is not unusual for creating DSLs in mainstream languages. Sean McDirmid uses similar tricks for his C# Bling library for WPF, except that Bling must overcome the lack of C# offering comparable extensions to Scala.

Syntactic Proofs of Compositional Compiler Correctness

Semantic preservation by compilers for higher-order languages can be verified using simple syntactic methods. At the heart of classic techniques are relations between source-level and target-level values. Unfortunately, these relations are specific to particular compilers, leading to correctness theorems that have nothing to say about linking programs with functions compiled by other compilers or written by hand in the target language. Theorems based on logical relations manage to avoid this problem, but at a cost: standard logical relations do not apply directly to programs with non-termination or impurity, and extensions to handle those features are relatively complicated, compared to the classical compiler verification literature.

In this paper, we present a new approach to “open” compiler correctness theorems that is “syntactic” in the sense that the core relations do not refer to semantics. Though the technique is much more elementary than previous proposals, it scales up nicely to realistic languages. In particular, untyped and impure programs may be handled simply, while previous work has addressed neither in this context.

Our approach is based on the observation that it is an unnecessary handicap to consider proofs as black boxes. We identify some theorem-specific proof skeletons, such that we can define an algebra of nondeterministic compilations and their proofs, and we can compose any two compilations to produce a correct-by-construction result. We have prototyped these ideas with a Coq implementation of multiple CPS translations for an untyped Mini-ML source language with recursive functions, sums, products, mutable references, and exceptions.

A submitted draft of another paper from Adam, continuing to expand LambdaTamer's reach.