The Logical Basis of System Correctness

Robert L. Constable
Cornell University

2005

Abstract:

The principal focus of these lectures will be the synthesis of algorithms and protocols from
constructive proofs that specifications are achievable. The practice of creating correct-byconstruction
functional and procedural programs is well established, and many examples are
widely known. We will briefly consider the functional case as a way of motivating the case of
distributed protocols.
The lectures will explain new synthesis techniques for distributed systems using the notion of
event structures and the associated logic of events developed by Mark Bickford and me starting
in 2003. My article in the proceedings of the 2005 summer school provides one example of
our approach. In these lectures I will systematically develop the new theory and illustrate the
synthesis method.
Much of the lecture material is on the Nuprl Web page at www.nuprl.org. It is included in
the section called Math Library.

Course Outline

Lecture 1 A Computation System and Functional Types
Lecture 2 Types and Classes
Lecture 3 Event Systems and Types for Concurrency
Lecture 4 A Logic of Events
Lecture 5 Proofs as Processes

References

1. Robert Constable, Information-intensive proof technology, MOD 2003 proceedings.
2. Robert Constable, Naive Computational Type Theory, Proof and System Reliability, (eds.
   H. Schwichtenberg, and R. Steinbruggen), Kluwer, 2002, pp 213-259.
3. Mark Bickford and Robert Constable, A Logic of Events, TR2003-1893, Cornell University,
   Computer Science Department.
4. Mark Bickford, Robert Constable, Joseph Halpern, Sabina Petride, Knowledge-Based Synthesis
   of Distributed Systems Using Event Structures, The 11th International Conference
   on Logic for Programming Artificial Intelligence and Reasoning (LPAR-11), Lecture Notes
   in Artificial Intelligence, Springer-Verlag, 2005. pp 449-465.
5. Nancy Lynch, Distributed Algorithms, Morgan Kaufman Publishers, 1996.
6. Mark Bickford, Event Systems, an on-line formalization, 2005,
   www.cs.cornell.edu/Info/People/sfa/Nuprl/EventSystems/