A Causal Logic of Events in Formalized Computational Type Theory
Book Article Version [PDF]
Tech Report Version
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-2010
unofficial copies
[PDF],
[PS]
by Mark Bickford and Robert L. Constable
Cornell University Technical Report 2005-2010, 2005.
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.