# 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**

- Robert Constable, Information-intensive proof technology, MOD 2003 proceedings.
- Robert Constable, Naive Computational Type Theory, Proof and System Reliability, (eds.

H. Schwichtenberg, and R. Steinbruggen), Kluwer, 2002, pp 213-259.
- Mark Bickford and Robert Constable, A Logic of Events, TR2003-1893, Cornell University,

Computer Science Department.
- 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.
- Nancy Lynch, Distributed Algorithms, Morgan Kaufman Publishers, 1996.
- Mark Bickford, Event Systems, an on-line formalization, 2005,

www.cs.cornell.edu/Info/People/sfa/Nuprl/EventSystems/