Alan Schmitt just posted an invitation to participate in this event which will take place at POPL. I think anyone who can attend should.
An amusing historical analysis of the origin of zero based array indexing (hint: C wasn't the first). There's a twist to the story which I won't reveal, so as not to spoil the story for you. All in all, it's a nice anecdote, but it seems to me that many of the objections raised in the comments are valid.
The Université catholique de Louvain has joined the edX consortium this year, and as part of edX Peter Van Roy is preparing a MOOC (Massive Open Online Course) called Paradigms of Computer Programming starting next February.
As you'd expect the course uses the CTM book and is based on the course Peter has been teaching, it will thus present a multi-paradigm approach to programming and include non-traditional computational models such as the deterministic dataflow model for concurrent programming.
I wonder who will end up signing up for this course. I think the option of auditing might appeal to folks who found CTM interesting but are way beyond the category of beginning programmers for whom the course is officially designed.
This interesting blog post argues that in recent years Python has gained libraries making it the choice language for scientific computing (over MATLAB and R primarily).
I find the details discussed in the post interesting. Two small points that occur to me are that in several domains Mathematica is still the tool of choice. From what I could see nothing free, let alone open source, is even in the same ballpark in these cases. Second, I find it interesting that several of the people commenting mentioned IPython. It seems to be gaining ground as the primary environment many people use.
Pure Subtype Systems, by DeLesley S. Hutchins:
This paper introduces a new approach to type theory called pure subtype systems. Pure subtype systems differ from traditional approaches to type theory (such as pure type systems) because the theory is based on subtyping, rather than typing. Proper types and typing are completely absent from the theory; the subtype relation is defined directly over objects. The traditional typing relation is shown to be a special case of subtyping, so the loss of types comes without any loss of generality.
Pure subtype systems provide a uniform framework which seamlessly integrates subtyping with dependent and singleton types. The framework was designed as a theoretical foundation for several problems of practical interest, including mixin modules, virtual classes, and feature-oriented programming.
The cost of using pure subtype systems is the complexity of the meta-theory. We formulate the subtype relation as an abstract reduction system, and show that the theory is sound if the underlying reductions commute. We are able to show that the reductions commute locally, but have thus far been unable to show that they commute globally. Although the proof is incomplete, it is “close enough” to rule out obvious counter-examples. We present it as an open problem in type theory.
A thought-provoking take on type theory using subtyping as the foundation for all relations. He collapses the type hierarchy and unifies types and terms via the subtyping relation. This also has the side-effect of combining type checking and partial evaluation. Functions can accept "types" and can also return "types".
Of course, it's not all sunshine and roses. As the abstract explains, the metatheory is quite complicated and soundness is still an open question. Not too surprising considering type checking Type:Type is undecidable.
Hutchins' thesis is also available for a more thorough treatment. This work is all in pursuit of Hitchens' goal of feature-oriented programming.
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.
Nominations must be submitted to the secretary of SIGPLAN by January 5th 2014 to be considered for this year's award. The nominated dissertation must be available in an English language version to facilitate evaluation by the selection committee and have been awarded in the year 2013.
I know of some outstanding dissertations. I am sure you do to. So why not nominate them for this honor (for further details see here)?
Taking Off the Gloves with Reference Counting Immix, by Rifat Shahriyar, Stephen M. Blackburn, and Kathryn S. McKinley:
Despite some clear advantages and recent advances, reference counting remains a poor cousin to high-performance tracing garbage collectors. The advantages of reference counting include a) immediacy of reclamation, b) incrementality, and c) local scope of its operations. After decades of languishing with hopelessly bad performance, recent work narrowed the gap between reference counting and the fastest tracing collectors to within 10%. Though a major advance, this gap remains a substantial barrier to adoption in performance-conscious application domains. Our work identiﬁes heap organization as the principal source of the remaining performance gap. We present the design, implementation, and analysis of a new collector, RCImmix, that replaces reference counting’s traditional free-list heap organization with the line and block heap structure introduced by the Immix collector. The key innovations of RCImmix are 1) to combine traditional reference counts with per-line live object counts to identify reusable memory and 2) to eliminate fragmentation by integrating copying with reference counting of new objects and with backup tracing cycle collection. In RCImmix, reference counting offers efﬁcient collection and the line and block heap organization delivers excellent mutator locality and efﬁcient allocation. With these advances, RCImmix closes the 10% performance gap, outperforming a highly tuned production generational collector. By removing the performance barrier, this work transforms reference counting into a serious alternative for meeting high performance objectives for garbage collected languages.
A new reference counting GC based on the Immix heap layout, which purports to close the remaining performance gap with tracing collectors. It builds on last year's work, Down for the count? Getting reference counting back in the ring, which describes various optimizations to raw reference counting that make it competitive with basic tracing. There's a remaining 10% performance gap with generational tracing that RCImmix closes by using the Immix heap layout with bump pointer allocation (as opposed to free lists typically used in RC). The improved cache locality of allocation makes RCImmix even faster than the generational tracing Immix collector.
However, the bump pointer allocation reduces the incrementality of reference counting and would impact latency. One glaring omission of this paper is the absence of latency/pause time measurements, which is typical of reference counting papers since ref counting is inherently incremental. Since RCImmix trades off some incrementality for throughput by using bump pointer allocation and copy collection, I'm curious how this impacts the pause times.
Reference counting has been discussed a few times here before, and some papers on past ref-counting GC's have been posted in comments, but this seems to be the first top-level post on competitive reference counting GC.
LVars are one outcome of Lindsey Kuper's ongoing
PhD work at Indiana University. They generalize existing models for
deterministic parallelism by considering a general framework of
monotonic read and write operations. They were briefly mentioned
on LtU before (along with the strongly related work on Bloom in the distributed
systems community), and were recently presented in two
distinct and complementary articles.
The first article describes the basic building blocks and ideas of LVars:
LVars: Lattice-Based Data Structures for Deterministic Parallelism
Lindsey Kuper, Ryan R. Newton
Programs written using a deterministic-by-construction model of
parallel computation are guaranteed to always produce the same
observable results, offering programmers freedom from subtle,
hard-to-reproduce nondeterministic bugs that are the scourge of
parallel software. We present LVars, a new model for deterministic-
by-construction parallel programming that generalizes existing
single-assignment models to allow multiple assignments that are
monotonically increasing with respect to a user-specified lattice.
LVars ensure determinism by allowing only monotonic writes and
"threshold" reads that block until a lower bound is reached. We
give a proof of determinism and a prototype implementation for a
language with LVars and describe how to extend the LVars model
to support a limited form of nondeterminism that admits failures
but never wrong answers
The second relaxes the original model by introducing failure, which
widens its applicability:
Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars
Lindsey Kuper, Aaron Turon, Neelakantan Krishnaswami, Ryan R. Newton
Deterministic-by-construction parallel programming models offer
programmers the promise of freedom from subtle, hard-to-reproduce
nondeterministic bugs in parallel code. A principled approach to
deterministic-by-construction parallel programming with shared state
is offered by LVars: shared memory locations whose semantics are
defined in terms of a user-specified lattice. Writes to an LVar take
the least upper bound of the old and new values with respect to the
lattice, while reads from an LVar can observe only that its contents
have crossed a specified threshold in the lattice. Although it
guarantees determinism, this interface is quite limited.
We extend LVars in two ways. First, we add the ability to “freeze”
and then read the contents of an LVar directly. Second, we add the
ability to attach callback functions to an LVar, allowing events to be
triggered by writes to it. Together, callbacks and freezing enable
an expressive and useful style of parallel programming. We prove that
in a language where communication takes place through freezable LVars,
programs are at worst quasi-deterministic: on every run, they either
produce the same answer or raise an error. We demonstrate the
viability of our approach by implementing a library for Haskell
supporting a variety of LVar-based data structures, together with
two case studies that illustrate the programming model and yield
promising parallel speedup.
Something I personally found surprising and impressive about LVars is
that, while I was initially interested in the very formal aspects of
providing a theoretical framework for deterministic concurrency, it
very quickly produced a practical library that people can use to write
parallel program -- and competitive with existing high-performance
approaches. As described in a
recent blog post, a Haskell library is available on Hackage -- but
surely LVars-inspired libraries could make sense in a lot of other
languages as well.
Andreas Abel and Brigitte Pientka's Well-Founded
Recursion with Copatterns; a Unified Approach to Termination and
Productivity is one of my highlights of the just-finished ICFP
2013, but it makes sense to focus on the first paper on this work,
published at POPL back in January.
Copatterns: Programming Infinite Structures by Observations
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
Inductive datatypes provide mechanisms to define finite data such as
finite lists and trees via constructors and allow programmers to
analyze and manipulate finite data via pattern matching. In this
paper, we develop a dual approach for working with infinite data
structures such as streams. Infinite data inhabits coinductive
datatypes which denote greatest fixpoints. Unlike finite data which is
defined by constructors we define infinite data by observations. Dual
to pattern matching, a tool for analyzing finite data, we develop the
concept of copattern matching, which allows us to synthesize infinite
data. This leads to a symmetric language design where pattern matching
on finite and infinite data can be mixed. We present a core language
for programming with infinite structures by observations together with
its operational semantics based on (co)pattern matching and describe
coverage of copatterns. Our language naturally supports both
call-by-name and call-by-value interpretations and can be seamlessly
integrated into existing languages like Haskell and ML. We prove type
soundness for our language and sketch how copatterns open new
directions for solving problems in the interaction of coinductive and
Codata has been often discussed here and elsewhere. See notably the
discussion on Turner's Total Functional
Programming (historical note: this 2004 beautification of the
original 1995 paper which had much of the same ideas), and on the
language. Given those precedents, it would be easy for the quick
reader to "meh" on the novelty of putting "observation" first
(elimination rather than introduction rules) when talking about
codata; yet the above paper is the first concrete, usable presentation
of an observation in a practical setting that feels right,
and it solves long-standing problem that current dependently-typed
languages (Coq and Agda) have.
Coinduction has an even more prominent role, due to its massive use
to define program equivalence in concurrent process calculi; the
relevant LtU discussion being about Davide Sangiorgi's On the origins of
Bisimulation, Coinduction, and Fixed Points. The POPL'13 paper
doesn't really tell us how coinduction should be seen with
copatterns. It does not adress the question of termination, which is
the topic of the more recent ICFP'13 paper, but I would say that the
answer on that point feels less definitive.