Lambda the Ultimate

Subscribe to Lambda the Ultimate feed
Updated: 2 hours 56 min ago

John C Reynolds Doctoral Dissertation Award nominations for 2014

Wed, 11/26/2014 - 22:05



Presented annually to the author of the outstanding doctoral dissertation in the area of Programming Languages. The award includes a prize of $1,000. The winner can choose to receive the award at ICFP, OOPSLA, POPL, or PLDI.

I guess it is fairly obvious why professors should propose their students (the deadline is January 4th 2015). Newly minted PhD should, for similar reasons, make sure their professors are reminded of these reasons. I can tell you that the competition is going to be tough this year; but hey, you didn't go into programming language theory thinking it is going to be easy, did you?

Zélus : A Synchronous Language with ODEs

Sat, 11/22/2014 - 18:31



Zélus : A Synchronous Language with ODEs
Timothy Bourke, Marc Pouzet

Zélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data-flow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code.

A dedicated type system and causality analysis ensure that all discrete changes are aligned with zero-crossing events so that no side effects or discontinuities occur during integration. Programs are statically scheduled and translated into sequential code that, by construction, runs in bounded time and space. Compilation is effected by source-to-source translation into a small synchronous subset which is processed by a standard synchronous compiler architecture. The resultant code is paired with an off-the-shelf numeric solver.

We show that it is possible to build a modeler for explicit hybrid systems à la Simulink/Stateflow on top of an existing synchronous language, using it both as a semantic basis and as a target for code generation.

Synchronous programming languages (à la Lucid Synchrone) are language designs for reactive systems with discrete time. Zélus extends them gracefully to hybrid discrete/continuous systems, to interact with the physical world, or simulate it -- while preserving their strong semantic qualities.

The paper is short (6 pages) and centered around examples rather than the theory -- I enjoyed it. Not being familiar with the domain, I was unsure what the "zero-crossings" mentioned in the introductions are, but there is a good explanation further down in the paper:

The standard way to detect events in a numeric solver is via zero-crossings where a solver monitors expressions for changes in sign and then, if they are detected, searches for a more precise instant of crossing.

The Zélus website has a 'publications' page with more advanced material, and an 'examples' page with case studies.

Facebook releases "Flow", a statically typed JavaScript variant

Tue, 11/18/2014 - 19:19



The goal of Flow is to find errors in JavaScript code with little programmer effort. Flow relies heavily on type inference to find type errors even when the program has not been annotated - it precisely tracks the types of variables as they flow through the program.

At the same time, Flow is a gradual type system. Any parts of your program that are dynamic in nature can easily bypass the type checker, so you can mix statically typed code with dynamic code.

Flow also supports a highly expressive type language. Flow types can express much more fine-grained distinctions than traditional type systems. For example, Flow helps you catch errors involving null, unlike most type systems.

Read more here.
Here's the announcement from Facebook.

Why do we need modules at all?

Wed, 11/05/2014 - 23:56



Post by Joe Armstrong of Erlang fame. Leader:

Why do we need modules at all? This is a brain-dump-stream-of-consciousness-thing. I've been thinking about this for a while. I'm proposing a slightly different way of programming here. The basic idea is:

  • do away with modules
  • all functions have unique distinct names
  • all functions have (lots of) meta data
  • all functions go into a global (searchable) Key-value database
  • we need letrec
  • contribution to open source can be as simple as contributing a single function
  • there are no "open source projects" - only "the open source Key-Value database of all functions"
  • Content is peer reviewed

Why does Erlang have modules? There's a good an bad side to modules. Good: Provides a unit of compilation, a unit of code distribution. unit of code replacement. Bad: It's very difficult to decide which module to put an individual function in. Break encapsulation (see later).

Conservation laws for free!

Tue, 10/28/2014 - 07:52



In this year's POPL, Bob Atkey made a splash by showing how to get from parametricity to conservation laws, via Noether's theorem:

Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds’ theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields “free” theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy, which by Noether’s theorem is a consequence of a system’s invariance under time-shifting.

In this paper, we link Reynolds’ relational parametricity with Noether’s theorem for deriving conserved quantities. We propose an extension of System Fω with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. We show, by constructing a relationally parametric model of our extension of Fω, that relational parametricity is enough to satisfy the hypotheses of Noether’s theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system.

Seemingly impossible programs

Wed, 10/22/2014 - 09:57



In case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:

Programming language semantics is typically applied to
prove compiler correctness and allow (manual or automatic) program
verification. Certain kinds of semantics can also be applied to
discover programs that one wouldn't have otherwise thought of. This is
the case, in particular, for semantics that incorporate topological
ingredients (limits, continuity, openness, compactness). For example,
it turns out that some function types (X -> Y) with X infinite (but
compact) do have decidable equality, contradicting perhaps popular
belief, but certainly not (higher-type) computability theory. More
generally, one can often check infinitely many cases in finite time.

I will show you such programs, run them fast in surprising instances,
and introduce the theory behind their derivation and working. In
particular, I will study a single (very high type) program that (i)
optimally plays sequential games of unbounded length, (ii) implements
the Tychonoff Theorem from topology (and builds finite-time search
functions for infinite sets), (iii) realizes the double-negation shift
from proof theory (and allows us to extract programs from classical
proofs that use the axiom of countable choice). There will be several
examples in the languages Haskell and Agda.

A shorter version (coded in Haskell) appears in Andrej Bauer's blog.

EATCS Award 2014: Gordon Plotkin

Sun, 10/12/2014 - 22:54



Gordon Plotkin is renowned for his groundbreaking contributions to programming language semantics, which have helped to shape the landscape of theoretical computer science, and which have im-pacted upon the design of programming languages and their verification technologies. The in-fluence of his pioneering work on logical frameworks pervades modern proof technologies. In addition, he has made outstanding contributions in machine learning, automated theorem prov-ing, and computer-assisted reasoning. He is still active in research at the topmost level, with his current activities placing him at the forefront of fields as diverse as programming semantics, applied logic, and systems biology.

Well deserved, of course. Congrats!

CFP: Off-the-Beaten-Track (OBT) workshop at POPL 2015

Sun, 10/05/2014 - 15:59



Announcing the 2015 edition of the OBT workshop, to be co-located with POPL 2015, in Mumbai, India. Two-page paper submissions are due November 7, 2014.

From the web page (

Programming language researchers have the principles, tools, algorithms and abstractions to solve all kinds of problems, in all areas of computer science. However, identifying and evaluating new problems, particularly those that lie outside the typical core PL problems we all know and love, can be a significant challenge. This workshop's goal is to identify and discuss problems that do not often show up in our top conferences, but where programming language research can make a substantial impact. We hope fora like this will increase the diversity of problems that are studied by PL researchers and thus increase our community's impact on the world.

While many workshops associated with POPL have become more like mini-conferences themselves, this is an anti-goal for OBT. The workshop will be informal and structured to encourage discussion. We are at least as interested in problems as in solutions.

Domain settings

Sat, 10/04/2014 - 11:24



I am about to make some changes to the name server definitions. Since changes take time to propagate, you may have trouble reaching the site for awhile. If this happens, try using the .com domain instead of the preferred .org domain.

Tue, 09/30/2014 - 19:27



In his blog, Bob Harper, in joint effort with Dave MacQueen and Lars Bergstrom, announces the launch of

The Standard ML Family project provides a home for online versions of various formal definitions of Standard ML, including the "Definition of Standard ML, Revised" (Standard ML 97). The site also supports coordination between different implementations of the Standard ML (SML) programming language by maintaining common resources such as the documentation for the Standard ML Basis Library and standard test suites. The goal is to increase compatibility and resource sharing between Standard ML implementations.

The site includes a history section devoted to the history of ML, and of Standard ML in particular. This section will contain a collection of original source documents relating to the design of the language.

Inferring algebraic effects

Sat, 09/27/2014 - 23:16



Logical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:

We present a complete polymorphic effect inference algorithm for an ML-style language with handlers of not only exceptions, but of any other algebraic effect such as input & output, mutable references and many others. Our main aim is to offer the programmer a useful insight into the effectful behaviour of programs. Handlers help here by cutting down possible effects and the resulting lengthy output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred information from the programmer.

Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial.

LtU's new server

Tue, 09/23/2014 - 07:26



Lambda the Ultimate is now running on a new, faster, more reliable server. The old one is now, uh... pining for the fjords.

This should resolve the increasingly frequent outages we've seen recently.

Because the old server had started failing, we didn't have time to do as much quality control on the migration as we would have liked. If anyone notices any issues with the site, please comment in this thread.

Currently known issues:

  • Non-Latin UTF-8 characters apparently didn't survive the database migration correctly. This is a particular issue if you have a username containing non-Latin characters - you may not be able to log in currently.
  • It's possible that some comments posted later on Monday don't appear on the new site.
  • New user signup emails are not yet working.
  • Due to DNS propagation, not everyone will see the new site immediately.

The above issues should be resolved sometime on Tuesday.

Breaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures

Mon, 09/22/2014 - 14:10



Breaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures by Pieter Wuille and Tom Schrijvers:

Pure functional programming language offer many advantages over impure languages. Unfortunately, the absence of destructive update, imposes a complexity barrier. In imperative languages, there are algorithms and data structures with better complexity. We present our project for combining existing program transformation techniques to transform inefficient pure data structures into impure ones with better complexity. As a consequence, the programmer is not exposed to the impurity and retains the advantages of purity.

This paper is along the same lines a question I asked a couple of years ago. The idea here is to allow programming using immutable interfaces, and then automatically transform it into a more efficient mutable equivalent.

An operational and axiomatic semantics for non-determinism and sequence points in C

Sun, 09/14/2014 - 09:36



In a recent LtU discussion, naasking comments that "I always thought languages that don't specify evaluation order should classify possibly effectful expressions that assume an evaluation order to be errors". Recent work on the C language has provided reasonable formal tools to reason about evaluation order for C, which has very complex evaluation-order rules.

An operational and axiomatic semantics for non-determinism and sequence points in C
Robbert Krebbers

The C11 standard of the C programming language does not specify the execution order of expressions. Besides, to make more effective optimizations possible (e.g. delaying of side-effects and interleav- ing), it gives compilers in certain cases the freedom to use even more behaviors than just those of all execution orders.

Widely used C compilers actually exploit this freedom given by the C standard for optimizations, so it should be taken seriously in formal verification. This paper presents an operational and ax- iomatic semantics (based on separation logic) for non-determinism and sequence points in C. We prove soundness of our axiomatic se- mantics with respect to our operational semantics. This proof has been fully formalized using the Coq proof assistant.

One aspect of this work that I find particularly interesting is that it provides a program (separation) logic: there is a set of inference rules for a judgment of the form \(\Delta; J; R \vdash \{P\} s \{Q\}\), where \(s\) is a C statement and \(P, Q\) are logical pre,post-conditions such that if it holds, then the statement \(s\) has no undefined behavior related to expression evaluation order. This opens the door to practical verification that existing C program are safe in a very strong way (this is all validated in the Coq theorem prover).

Luca Cardelli Festschrift

Fri, 09/12/2014 - 10:10



Earlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:

Luca Cardelli has made exceptional contributions to the world of programming
languages and beyond. Throughout his career, he has re-invented himself every
decade or so, while continuing to make true innovations. His achievements span
many areas: software; language design, including experimental languages;
programming language foundations; and the interaction of programming languages
and biology. These achievements form the basis of his lasting scientific leadership
and his wide impact.
Luca is always asking "what is new", and is always looking to
the future. Therefore, we have asked authors to produce short pieces that would
indicate where they are today and where they are going. Some of the resulting
pieces are short scientific papers, or abridged versions of longer papers; others are
less technical, with thoughts on the past and ideas for the future. We hope that
they will all interest Luca.

Hopefully the videos will be posted soon.

Re-thinking Prolog

Thu, 09/11/2014 - 14:31



A recent paper by Oleg Kiselyov and Yukiyoshi Kameyama at the university of Tsukuba discusses weaknesses and areas for improvement to Prolog.

Quite many computations and models are mostly deterministic. Implementing them in Prolog with any acceptable performance requires the extensive use of problematic features such as cut. Purity is also compromised when interfacing with mainstream language libraries, which are deterministic and cannot run backwards. Divergence is the constant threat, forcing the Prolog programmers to forsake the declarative specification and program directly against the search strategy. All in all, Classical Prolog is the exquisite square peg in the world with mostly round holes

The strong points of Prolog can be brought into an ordinary functional programming language. Using OCaml as a representative, we implement lazy guessing as a library, with which we reproduce classical Prolog examples. Furthermore, we demonstrate parser combinators that use committed choice (maximal munch) and can still be run forwards and backwards. They cannot be written in Classical Prolog. Logic variables, unification, and its WAM compilation strategy naturally emerge as a "mere optimization" of the Herbrand universe enumeration.

The paper mentions the strength of the approach used by miniKanren (which embeds logic programming with fairer search strategy than normal Prolog into Scheme) and Hansei (which embeds probability based nondeterminism into Ocaml using delimited continuations to allow direct-style expression of monadic code).

After motivating some choices by studying the prototypical example of running append backwards they cover running parsers with "maximal munch" rule backwards - something that cannot be (declaratively) expressed in prolog.

A very interesting paper on logic programming! It also thanks Tom Schrijvers of CHR fame at the end.

Scratch jr

Sat, 09/06/2014 - 17:45



Scratch jr is an iPad version of the Scratch environment, designed with young kids in mind. It is the best kid-oriented programming tool I tried so far, and my five year old has great fun making "movies" with it. As I noted on twitter an hour after installing, the ability to record your own voice and use it for your sprites is a killer feature. Check it out!

Scala woes?

Sat, 09/06/2014 - 12:12



A fork in the back? See discussion over at HN. People in the know are encouraged to shed light on the situation.