Systems Outage: June 30 - July 2

More info at

Blog from November, 2007

SIGACT News Logic Column 20

The new SIGACT News Logic Column is available. It is very short, consisting of the synopsis of Simon Kramer's Ph.D. Thesis from l'École Polytechnique Fédérale de Lausanne, Logical Concepts in Cryptography.

As I state in the editorial blurb, Simon introduces a new logic for reasoning about cryptographic protocol called CPL (Cryptographic Protocol Logic). The result is an intriguing blend of modal logic and process algebra, reminiscent of spatial logics for process calculi, but extended with knowledge, belief, and provability operators.

On Coinduction

A slow weekend - I needed the rest.

Dexter Kozen just uploaded an article on Coinductive Proof Principles for Stochastic Processes to CoRR, wherein he gives "an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process." I looked at this paper a while back, and it remains interesting.

On a different bit of news, the CSLI Lecture Notes are now freely available online, gracieuseté of the Stanford Medieval and Modern Thought Text Digitization Project.

That series includes the classics

  • Troelstra's Lectures on Linear Logic
  • Goldblatt's Logic of Time and Computation

and to remain in the spirit of coinduction, two of the core monographs on the theoretical foundations of coinduction:

  • Aczel's Non-well-founded Sets
  • Barwise and Moss's Vicious Circles : On the Mathematics of Non-wellfounded Phenomena

(via Richard Zach's LogBlog)

J Strother Moore's Visit to NU

J. Strother Moore, the Moore in Boyer-Moore, just completed a two-days visit to Northeastern. He gave a talk, Machines Reasoning about Machines, complete with demo using the ACL2 theorem prover. ACL2 is a first-order theorem prover for proving equational properties of programs written in an applicative subset of Common Lisp. It is amazingly fast, and comes with a well-equipped library of theories to work with.

Fascinating work, if only because I am set to teach an undergraduate course using ACL2 next semester with Pete Manolios.

Now if we could just move the ACL2 technology to a typed language and extend it to higher-order, I'd be happy. (I know, I know, there are fundamental limitations re the latter, but still, even getting halfway there would be fun.)

Pete told me that the two books on ACL2:

  • Computer-Aided Reasoning: An Approach
  • Computer-Aided Reasoning: ACL2 Case Studies

are now available in paperback for a very reasonable fee.