Summer Reading

8 06 2011

I’m headed back to Microsoft for the summer, to do some program analysis work.  I’ve got quite a lengthy commute from where I live in Seattle, which should be made much more bearable by the Microsoft Connector bus.  Since I won’t be driving, I should have plenty of time to get some reading done.  My reading goals for the summer are to work my way through:

  • Type Theory and Functional Programming: An older (1991) book on type theory as in (dependent) constructive type theory, that appears to also (so far) do a good job connecting type theory to logic.  It’s hard to find a thorough reference that builds up to dependent types as they’re related to proofs and programs, from first principles of logic.  I believe there’s some overlap between this book and the next (Coq’Art), but TTFP is so far a much gentler introduction than the first few chapters of Coq’Art.  And since it’s out of print, the author has generously posted a PDF version online, so it’s convenient and free in addition to useful.
  • Coq’Art: Interactive Theorem Proving and Program Development: The reference on using Coq for proofs and program development.  Thorough, but dense so far.  It seems mostly focused on the use of Coq, but covers the underlying Calculus of Inductive Constructions as well.  After discovering first-hand how painful it can be to maintain a proof by hand as a formal system evolves, I’d really like to formalize all of my future proofs in a mechanized proof assistant.  And I have a desire to do some work on a Ynot-style embedding of a richly typed language.
  • Lambda-Calculus and Combinators: An Introduction: Covers what you’d expect from the title: connections between the lambda calculus and combinatory logic.
  • Semantics Engineering with PLT Redex: Covers some core background on specifying abstract machines (normally spread across many older papers), as well as the use of PLT Redex.  The authors to a good job of articulating the structure and purpose of the book here.
Quite a substantial undertaking to be done all outside of work (while still having a life), but I should at least be able to make a dent in things.  The fact that there’s some overlap in material among all of these books should also make it easier to get through all of them (and help the overlapping material sink in).  I’m already almost a third of the way through TTFP.  I’m not sure what order I’ll read the others, but I’m excited about all of them.

WordPress for iPhone Bug

23 07 2008

The few of you who subscribe to this blog’s RSS feed may have noticed a post with the title “!$title$!” preceding this post briefly.  Apparently this is a known bug in the recently released WordPress application for the iPhone. For many users, as soon as you add your account to the program or if you open a new post then back out of it, the program makes a test entry and leaves it.  This bug is so easy to trigger, I’m surprised it made it out the door (or that a random ‘test post’ function made it in the final product at all).

Amazon’s Book Recommendation System is Quirky

15 03 2008

Like many others, I have an wishlist, allow them to track my purchases, and occasionally tell them that I own a particular book if it is recommended to me.  Amazon uses this along with purchase sets made by other customers to generate “better” recommendations for books I might find interesting.  One thing its recommendation algorithm doesn’t seem to take into account is general subject knowledge – it knows of subcategories, and purchases of multiple items by the same people, but has no concept of actual relationships between books in a category.  This is actually a pretty reasonable thing to omit since there’s a great deal of such knowledge which could be taken into account, and the work/reward ratio for maintaining that is probably not great.  But as a result, I’ve had some rather interesting recommendations.

Also, I’m linking to books for clarity, but there’s no Amazon referral crap going on.

Mathematics texts.  Books on my Amazon wishlist: Foundations of Mathematical Logic, The Calculi of Lambda Conversion, Mathematical Foundations of Information Theory, Categories for the Working Mathematician, Basic Category Theory for Computer Scientists, among others.  Some of the more amusing mathematics recommendations from Amazon: Pre-Algebra, Algebra 2.

Literature.  Books on my Amazon Wishlist: Going After Cacciato, Letters to a Young Poet, The Norton Anthology of Poetry, ‘Tis: A Memoir, The Dharma Bums, among others.  Amazon recommends: Vocabulary Workshop: Level C.

These are just the few that I dug up spending a couple minutes searching my emailed recommendations; I’ve seen plenty more out of place recommendations upon logging into  While it’s certainly true that some people will buy books at both extremes of a field’s complexity (perhaps something advanced for themselves or a friend, and something basic for a child), it’s still an amusing quirk to have this disparity with recommendations for an individual because of the presentation. presents recommendations as a set of items you should be interested in according to Amazon’s “understanding” of your personal interests, when it’s really just correlating your purchases and explicit interests with the purchases of other users.