Lambda the Ultimate

A Lambda Calculus for Real Analysis

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function "hovers" near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.

Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX.

We present Joe-E, a language designed to support the development of secure software systems. Joe-E is a subset of Java that makes it easier to architect and implement programs with strong security properties that can be checked during a security review. It enables programmers to apply the principle of least privilege to their programs; implement application-specific reference monitors that cannot be bypassed; introduce and use domain-specific security abstractions; safely execute and interact with untrusted code; and build secure, extensible systems. Joe-E demonstrates how it is possible to achieve the strong security properties of an object-capability language while retaining the features and feel of a mainstream object-oriented language...

Section 5.2 discuss how Joe-E leverages Java static typing. Joe-E is implemented as a source-code verifier not a bytecode verifier. Section 6 of the paper explains this design choice.

Joe-E was mentioned on LtU in the past and is available here.

Quantum theory has acquired a reputation as an impenetrable theory accessible only after acquiring a significant theoretical physics background. One of the lessons of quantum computing is that this is not necessarily true: quantum computing can be learned without mastering vast amounts of physics, but instead by learning a few simple differences between quantum and classical information.

A well written article in the CACM.

There's also slides for a talk by Rob Pike on the same topic.

Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. "A few billion lines of code later: using static analysis to find bugs in the real world", Communications of the ACM, Volume 53, Issue 2, February 2010, Pages 66-75.

How Coverity built a bug-finding tool, and a business, around the unlimited supply of bugs in software systems.

This is a fascinating piece by Dawson Engler & co. on their experiences in commercializing their static analysis research through Coverity. It's an entertaining read, with many interesting anecdotes from various customers. But it also contains a number of useful insights about the difference between a research tool and a commercial product, the kinds of static analyses that do and don't make sense in a commercial context, and the multitude of problems caused by the lack of programming language standardization:

Checking code deeply requires understanding the code's semantics. The most basic requirement is that you parse it. Parsing is considered a solved problem. Unfortunately, this view is naïve, rooted in the widely believed myth that programming languages exist.

There's a lot of useful information in there for anyone interested in industrial-strength static analysis. There are also a lot of worthwhile things to keep in mind if you're designing a programming language, and want to make sure it's as friendly as possible to future static analysis tools.

Microsoft employee Bart De Smet, who has a widely trafficked blog, has been writing a lot in the past few months about a new library being designed by his group at Microsoft. Here is a whole truckload of blogpost links, in chronological order, which appears to be how Bart intended folks to read it:

Dec 26, 2009: More LINQ with System.Interactive – The Ultimate Imperative
Dec 27, 2009: More LINQ with System.Interactive – Exceptional Exception Handling
Dec 28, 2009: More LINQ with System.Interactive – Sequences under construction
Dec 29, 2009: More LINQ with System.Interactive – Exploiting the code = data relationship
Dec 30, 2009: More LINQ with System.Interactive – More combinators for your Swiss Army Knife
Jan 01, 2010: The Essence of LINQ – MinLINQ
Jan 07, 2010: More LINQ with System.Interactive – Functional fun and taming side-effects

I don't usually read blogs, but I thought this was a pretty cogent series of posts. Also, judging by how interested LtU and the surrounding blogosphere community was from Erik Meijer's presentation on the Rx framework at the JVM Language Summit 2009, I figured people would like this as well.

End-User Programming has been a topical discussion lately in mainstream software outlets. The IEEE journal Software recently had an issue dedicated to end-user programming challenges; see Joel Brandt's Opportunistic Programming: Writing Code to Prototype, Ideate and Discover and Martin Erwig's Software Engineering for Spreadsheets. Also, a few years ago a consortium of universities formed End-Users Shaping Effective Software, which includes Martin Erwig's PLT work on bringing type systems to spreadsheets.

Recently, Google invited Allen Cypher to give a TechTalk on The Evolution of End-User Programming, which appears to be a recapitulation of his VL/HCC paper by the same name. Allen was the editor of Watch What I Do (an LtU recommended reading).

Towards the end of the talk, Allen mentions the practical issues of knowing when to use what tool, and that novice users struggle with finding the right tool for the right job. What's notable about discussion of end-user software engineering is how little attention its proponents pay to its critics biggest criticism: Security. In the IEEE Software realm, probably the most open critic has been Warren Harrison (see: The Dangers of End-User Programming). For example, Ko's 2009 ACM Computing Survey The State of the Art in End-User Software Engineering only mentions security once, in the context of designing end-user description languages for security, but does not assess how well this technique compares to techniques software engineers might employ. It seems strange that leading researchers in visual languages and end-user programming do not discuss the potential usage of object capability systems, especially as companies try to monetize a percentage of the value added by users who mash-up their service with other services.

The introductory chapters are probably going to be unnecessary for LtU readers, but once things get going there is a lot to learn here if you are interested in formal semantics of natural language, especially in the Montague-style. And if this doesn't ring a bell - just search for "continutation" in the manuscript, and be prepared to meet old friends (you know who you are) in a new context.

If the contributing editors will neglect their duties, LtU will wither and die. Hint, hint.

Resolving and Exploiting the k-CFA Paradox, Matthew Might, Yannis Smaragdakis, and David Van Horn. To appear in PLDI 2010.

Low-level program analysis is a fundamental problem, taking the shape of "flow analysis" in functional languages and "points-to" analysis in imperative and object-oriented (OO) languages. Despite the similarities, the vocabulary and results in the two communities remain largely distinct, with limited cross-understanding. One of the few links is Shivers's k-CFA work, which has advanced the concept of "context-sensitive analysis" and is widely known in both communities. Recent results, however, indicate that the relationship between the different incarnations of the analysis is not understood.

Van Horn and Mairson proved k-CFA for k ≥ 1 to be EXPTIME-complete, hence no polynomial algorithm exists. Yet there have been multiple polynomial formulations of context-sensitive points-to analyses in OO languages. Is functional k-CFA a profoundly different analysis from OO k-CFA? We resolve this paradox by showing that OO features conspire to make the exact same specification of k-CFA be polynomial-time: objects and closures are subtly different, in a way that interacts crucially with context-sensitivity. This leads to a significant practical result: by emulating the OO approximation, we derive a polynomial hierarchy of context-sensitive CFAs for functional programs, simultaneously achieving high precision and efficiency.

I learned that performance bounds on flow analysis were fascinating from earlier work by David van Horn and Harry Mairson, so it's good to see that this line of work is still being continued, and even better to see new algorithms come out of it.

Continuity Analysis of Programs, Swarat Chaudhuri, Sumit Galwani, and Roberto Lublinerman. POPL 2010.

We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the robustness of programs whose inputs can have small amounts of error and uncertainty -- e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data.

Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate “synchronization points” between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.

We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.

Another fun paper from POPL this year. I've seen metric spaces used to solve domain equations before, but the idea of actually considering a metric on the outputs was a new one to me.

Monads in Action, Andrzej Filinski, POPL 2010.

In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be evaluated according to an effect-free semantics. Any effect-specific operations expressible in the monad are also given purely functional definitions, but these definitions are only directly executable in the context of an already translated program. This approach thus takes an inherently Church-style view of effects: the nominal meaning of every effectful term in the program depends crucially on its type.

We present here a complementary, operational view of monadic effects, in which an effect definition directly induces an imperative behavior of the new operations expressible in the monad. This behavior is formalized as additional operational rules for only the new constructs; it does not require any structural changes to the evaluation judgment. Specifically, we give a small-step operational semantics of a prototypical functional language supporting programmer-definable, layered effects, and show how this semantics naturally supports reasoning by familiar syntactic techniques, such as showing soundness of a Curry-style effect-type system by the progress+preservation method.

The idea of monadic reflection was one I never felt I really understood properly until I read this paper, so now I'll have to go back and re-read some of his older papers on the subject.