A Causal Logic of Events in Formalized Computational Type Theory
Book Article Version [PDF]
Tech Report Version
unofficial copies [PDF], [PS]
by Mark Bickford and Robert L. Constable
Cornell University Technical Report 2005-2010, 2005.
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.