Summer reading

For various reasons I haven't had time to make even semi-regular blog posts, so I thought I'd clear the decks a little by listing selected contents of my "recently read" basket, before I file them.

• Homotopy type theory: univalent foundations of mathematics and computation, Avigad et al.  (MURI proposal).  This is a public version of a large, recently funded project on homotopy type theory, and gives a good overview of what several of the leaders in this area think are the most interesting open problems.
• Towards Reversible Sessions, Tiezzi and Yoshida, PLACES 2014. Adapts the idea of reversibility to a setting with session types (though doesn't go into the actual type system)
• Free Theorems involving Type Constructor Classes (functional pearl), Janis Voigtländer, ICFP 2009.  Gives a high-level overview and several interesting examples of parametricity and free theorems in the presence of polymorphism over type constructors, possibly with class constraints (e.g. Monad m in Haskell)
• Computational logic and the social, Ursula Martin, Journal of Logic and Computation (advance access), 2014.  From a special issue dedicated to Roy Dyckhoff, whose MacLogic was one of the first interactive proof tools aimed at teaching logic.  Discusses computational proof tools in the context of social computation, crowdsourcing and the Web.  Proof has always been a partially social activity; mechanized proof has not always been welcomed by mathematicians because it is too formal. 
• Functorial data migration, David Spivak, Information and Computation 2012.  This work concerns using tools from category theory to model data and databases.  Essentially, objects are viewed as nodes in a graph, arrows as relationships, and data transformations are defined by taking pullbacks, left and right pushforwards from functors.  This paper is an interesting and accessible exposition, though it leaves a lot of questions that will, hopefully, be examined in future work.  Similar ideas seem to crop up frequently in the daabase theory community, particularly concerning data integration (e.g. "local as view", "global as view" mappings) and it would be interesting to see a rigorous categorical analysis of these ideas.
• A substructural logic for layered graphs, J. Logic and Computation, Collinson, McDonald and Pym.  Gives a semantic model and a bunched implications-like proof theory for graphs with a notion of "layering" or decomposition.