Tuesday, February 2, 2010
The current issue of CACM has an article on type theory:
When the philosopher Bertrand Russell invented type theory at the beginning of the 20th century, he could hardly have imagined that his solution to a simple logic paradox—defining the set of all sets not in themselves—would one day shape the trajectory of 21st century computer science.
It is riddled with misconceptions, errors, and self-aggrandizement. It does us the great disservice of conflating (dynamic) memory safety and (static) type safety, and has whoppers like “A type system ensures the correct behavior of any program routine by enforcing a set of predetermined behaviors,” which is just false. But hey, ra-ra types! No?
Some photos from POPL 2010 in Madrid, Spain.
Thursday, December 10, 2009
A new preprint by Matthew Might, Yannis Smaragdakis, and David Van Horn.
Abstract:
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.
Update (2/2010): This work will appear at PLDI 2010. See you in Toronto!
The Fortress folks have announced a new blog:
The Fortress team has started a blog, to post a series of
announcements and news items about Fortress. Our goal is to let
people know about ongoing technical discussions and decisions, as well
as the current status of the implementation. We will also post
interesting examples of Fortress code. We hope to put up new posts at
least weekly.
So far we have four posts. The first and fourth posts discuss the new
wiki markup for tables and images for use in Fortress comments; the
second post discusses some changes to the typing rules for conditional
expressions that will help them to interact better with coercion; the
third post reports on an implementation of the “treap” data structure
in Fortress. We also plan to report soon on the status of our efforts
to construct a Fortress compiler. Please visit
http://projectfortress.sun.com/Projects/Community/blog
or click on the “Blog” item at the right-hand end of the menu bar on
the main Wiki page.
The Higher-Order Flow Analysis Forum has just been set up:
The HOFA forum is an email forum for the discussion and dissemination of research results in the area of higher-order flow analysis, broadly construed, within computer science and related disciplines. Flow analysis and related static analyses are a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The HOFA forum aims to facilitate theoretical, practical, and application advances in the area of functional, object-oriented, concurrent, distributed, and mobile programming.
Please sign up! Also, send me email if you or your group would like to be listed on the HOFA site.
Saturday, September 26, 2009
Some photos from the 2009 Scheme and Functional Programming Workshop at Northeastern.
Wednesday, September 23, 2009
A new SRFI for inspecting the arity of procedures:
Many Scheme systems provide mechanisms for inspecting the arity of a procedural value, making it a common feature, however there is no standard interface. As a result there is no portable way to observe the arity of a procedure without actually applying it. This SRFI proposes a simple interface that is consistent with existing Scheme systems’ facilities and prior proposals.
Thursday, September 17, 2009
A new SRFI for purely functional random-access lists:
Functional programming and list hacking go together like peanut butter and jelly, eval and apply, syntax and semantics, or cursing and recursing. But the traditional approach to implementing pairs and lists results in index-based access (list-ref) requiring time proportional the index being accessed. Moreover, indexed-based functional update (list-set) becomes so inefficient as to be nearly unspeakable. Instead, programmers revert the imperatives of the state; they use a stateful data structure and imperative algorithms.
This SRFI intends to improve the situation by offering an alternative implementation strategy based on Okasaki’s purely functional random-access lists [1]. Random-access pairs and lists can be used as a replacement for traditional, sequential pairs and lists with no asymptotic loss of efficiency. In other words, the typical list and pair operations such as cons, car, and cdr, all operate in O(1) time as usual. However, random-access lists additionally support index-based access and functional update operations that are asymptotically cheaper; O(log n) for random-access lists versus O(n) for sequential-access lists, where n is the length of the list being access or updated. As such, many purely functional index-based list algorithms become feasible by using a random-access list representation for pairs and lists.
Tuesday, September 15, 2009
A new blog has been created for the Wand Symposium and Festschrift:
In the coming months, presenters and editors will be working on a Festschrift in honor of Mitch, as a special issue (or issues) or Higher-Order and Symbolic Computation. We’ll also be adding links to the presentation slides and videos as they become available. We’ll update this blog with developments.
Most of the slides from MitchFest are now available, too.
Slides from Mitch Wand’s keystone talk at the symposium in his honor. Required reading for any aspiring young scientist.