# * A Causal Logic of Events in Formalized Computational Type Theory *

## by Mark Bickford, Robert L. Constable

2005

- Presented at Logical Aspects of Secure Computer Systems, Proceedings of International Summer School Marktoberdorf
- unofficial PDF
- 2005 - Cornell University Technical Report http://hdl.handle.net/1813/5710

**Abstract**

We provide a logic for distributed computing that has the explanatory and technical
power of constructive logics of computation. In particular, we establish a proof technology
that supports correct-by-construction programming based on the notion that
concurrent processes can be extracted from proofs that specifications are achievable.

**bibTex ref: BC05**

cite link