Greetings from PLANETQUANTUM.COM. I've been toiling away on logic, interactive theorem proving (early stage), and pushing Quantum's interactive 2D graphics to a better stage. This year, among other things, I plan to look at:

• Calculemus conferences (Springer-Verlag)
• Compute Aided Verification conferences (Springer-Verlag)
• Existing work on theorem provers (e.g. ACL2, Mizar, MetaMath, HOL, Isabelle, Coq, PVS, ...)
• Existing work on program verification (e.g. AProVE, SATABS, CBMC, piVC, ...)
• Programming language design - state of the art

I'm thinking about updating the PLANETQUANTUM.COM online manual sometime this year...

And maybe staying in touch with my PLANETQUANTUM.COM readers a little more often. :-)

Here are a couple papers which I found interesting and I think are worth reading:

• Michael Beeson and Freek Wiedijk: The meaning of infinity in calculus and computer algebra systems, Journal of Symbolic Computation 39(5) (2005), pp. 523-538.
• "The Seventeen Provers of the World"
  http://www.cs.ru.nl/~freek/comparison/
  http://www.cs.ru.nl/~freek/comparison/diffs.ps.gz

Finally, here is a report on my trip to Paris, France: XMAS2009.