archives

Certified Programming with Dependent Types: home stretch!

For the last few years, I've been working on Certified Programming with Dependent Types, a book giving a pragmatic introduction to the Coq proof assistant. The drafts have been available for free online, and future versions should be as well; but I'm also working toward a traditional print version from MIT Press.

I've recently finished the last non-trivial content changes that I've had planned, so I write to you to ask for your help in finding the last mistakes and opportunities for improvement! Once everything is in good shape, I can move forward with traditional publication.

There are a few categories of known issues. One is font choice and other typesetting; this is coming from coqdoc, Coq's documentation generation program, and I expect to need to jump into the coqdoc source code to an extent, to get everything looking pretty without excessive countermeasures in the book source code.

Where I could especially use help is finding appropriate citations to research papers and so on. There are few subjects that I'm already looking for the right citations on, and I figure LtU is a great place to find people who have favorites in these categories. So, could you please let me know if you have a citation to recommend for any of the following?

  • the concept of continuation and/or continuation-passing style
  • the concept of unification
  • infinite data structures in Haskell
  • Haskell "deriving" clauses
  • some introduction to logic programming, to cite in lieu of going into full detail on the usual foundations of the paradigm

I'll also appreciate advice on any other points in the text that you think deserve citations, and I'll appreciate suggestions the most if they come with suggested citation targets. :)

And any other finding of typos, confusing prose, and so on will be much appreciated! You can e-mail me or reply to this post, as seems appropriate.

Thanks in advance! I'm looking forward to getting the book out there.