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!
No comments:
Post a Comment
Note: Only a member of this blog may post a comment.