A Causal Logic of Events in Formalized Computational Type Theory
by Mark Bickford, Robert L. Constable
- 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
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