▶ Nested Refinements: A Logic For Duck Typing (via @swannodette)
Programs written in dynamic languages make heavy use of features — run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions — that are beyond the reach of type systems that employ either purely syntactic or purely semantic reasoning. We present a core calculus, System D, that merges these two modes of reasoning into a single powerful mechanism of nested re- ﬁnement types wherein the typing relation is itself a predicate in the reﬁnement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested reﬁnements with McCarthy’s theory of ﬁnite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the reﬁnement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratiﬁcation approach that we use to prove the soundness of System D.(See also The Shadow Superpower: the $10 trillion global black market is the world's fastest growing economy: "System D is a slang phrase pirated from French-speaking Africa and the Caribbean. The French have a word that they often use to describe particularly effective and motivated people. They call them débrouillards. To say a man is a débrouillard is to tell people how resourceful and ingenious he is.")
▶ Dart Talk @ Stanford (I think this is by Bracha. Haven't checked it out coz it's in some weird Windows format.)
▶ Things SQL needs: MERGE JOIN that would seek (Nice idea about using histograms to speed up index scans. I believe the new App Engine query planner does that or something similar. Also Understanding Histograms in Oracle.)
▶ I'm a big fan of the tagless-final approach! (This comment caught my interest, because it reminds me of Kernel: "everything in the language has to become both directly interpretable and available as an AST".)
▶ New extension to Haskell -- data types and polymorphism at the type level (Ωmega-like.)
▶ Evolution of DDD: CQRS and Event Sourcing (@dyokomizo hyped this weird-sounding stuff in response to Beating the CAP theorem).
(* As Rob Zombie says: "I feel that the Nazi movie is back. Once the trend comes back, the Nazi trends comes back, now you pervert it like crazy and you add werewolves. So, I don't know if we'll ever see that movie, but now is the time. The time is now to strike with this.")