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.