**Systems Outage: June 30 - July 2**

More info at l.khoury.to/jun30-outage

search

attachments

weblink

advanced

Overview

Content Tools

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.

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.

- Coinductive Proof Principles for Stochastic Processes_, by D. Kozen.

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, 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.