POPL 2012 Papers

It's just a few weeks until POPL 2012 (Symposium on Principles of Programming Languages, one of the top programming language theory research conferences) in Philadelphia. The program has been out for a while. This time, there are three papers on C/C++ semantics. Apparently we have gotten to the point where researchers have (mechanically) formalized interesting chunks of that large, complicated edifice. The one coming out from INRIA [PDF] has a mechanized (Coq) semantics for C++ construction and destruction including C++11 features. The authors actually give a formal proof of the RAII (resource acquisition is initialization) pattern, specifically that in a terminating program every construction of a subobject is indeed matched by a destruction. The process of developing a formal semantics also helped identify issues in the C++ standard both C++03 and C++11. On the type systems side, there is also a paper from Adobe Research on gradual type systems, especially a type inference scheme with support for dynamic types. One paper describes a type system and language design supporting probability density functions for custom probability distributions and continuous probability. Apparently probability distributions are monads too!

Static Type System and Numerical Computing

The programming languages with which most people are familiar, such C/C++, Java, Python, JavaScript, and Ruby, presents a very stark contrast. On the one hand, you have statically typed languages (C/C++ and Java) which are amenable to a wide assortment of compile-time optimizations due to the presence of types. On the other, you have dynamically typed languages (Python, JavaScript, and Ruby) which are "fun" to program and amenable to rapid prototype due to more succinct syntax partly due to the absence of explicit type annotations. The sweet spot, in my humble opinion, is statically type but with type inference, a subject of my expertise and doctoral studies. I plan to write a few posts on this subject, near and dear to my heart. Heavy duty Numerical computing is one area where dynamically typed languages such as Matlab, R, and NumPy/Python have gained a considerable mindshare. Since NumPy offloads computations to efficient C libraries, this is quite reasonable. I would like to discuss where I think numerical computing and statistical analysis programs can benefit from a more sophisticated static type system with type inference. To whet your appetite, consider the case that C++'s Boost Library contains the functionality needed to statically check for units (i.e., dimensional analysis). The performance difference between code generated from statically typed languages and from dynamically typed languages is not just the absence of dynamic type checks. Types in static type systems enable a considerable array of optimizations to get rid of that last tiny ounce of latency.